From 2ece985abf0cfd7ef91b614f5f26d80dddb5e57a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 18 Mar 2026 13:26:55 +0100 Subject: [PATCH 1/2] Adapt to rocq-prover/rocq#21773 (sort poly cumulativity) --- template-rocq/src/ast_quoter.ml | 2 +- template-rocq/src/quoter.ml | 8 +++++++- template-rocq/src/run_template_monad.ml | 2 +- 3 files changed, 9 insertions(+), 3 deletions(-) diff --git a/template-rocq/src/ast_quoter.ml b/template-rocq/src/ast_quoter.ml index e4f337f41..074496aa7 100644 --- a/template-rocq/src/ast_quoter.ml +++ b/template-rocq/src/ast_quoter.ml @@ -355,7 +355,7 @@ struct mind_entry_inds = List.map quote_one_inductive_entry is; mind_entry_template = false; mind_entry_universes = univs; - mind_entry_variance = variance; + mind_entry_variance = Option.map (fun v -> [||], v) variance; mind_entry_private = None } let quote_definition_entry ty body ctx = diff --git a/template-rocq/src/quoter.ml b/template-rocq/src/quoter.ml index 5064c66f1..9d2c34bd8 100644 --- a/template-rocq/src/quoter.ml +++ b/template-rocq/src/quoter.ml @@ -464,7 +464,13 @@ struct let nparams = Q.quote_int mib.Declarations.mind_nparams in let paramsctx, acc = quote_rel_context quote_term acc env sigma mib.Declarations.mind_params_ctxt in let uctx = quote_universes_decl mib.Declarations.mind_universes mib.Declarations.mind_template in - let var = Option.map (CArray.map_to_list Q.quote_variance) mib.Declarations.mind_variance in + let var = match mib.Declarations.mind_variance with + | None -> None + | Some (qv,uv) -> + if not @@ CArray.is_empty qv then CErrors.user_err Pp.(str "Cumulative sort polymorphism not supported."); + Some uv + in + let var = Option.map (CArray.map_to_list Q.quote_variance) var in let bodies = List.map Q.mk_one_inductive_body (List.rev ls) in let finite = Q.quote_mind_finiteness mib.Declarations.mind_finite in (* let templatePoly = Q.quote_bool mi.mind_template in *) diff --git a/template-rocq/src/run_template_monad.ml b/template-rocq/src/run_template_monad.ml index 9ec3e4a12..88b5fdc2f 100644 --- a/template-rocq/src/run_template_monad.ml +++ b/template-rocq/src/run_template_monad.ml @@ -278,7 +278,7 @@ let unquote_mutual_inductive_entry env evm trm (* of type mutual_inductive_entry let evm, univs = denote_universes_entry env evm univs in let template = unquote_bool template in let variance = unquote_map_option - (fun v -> CArray.map_of_list (unquote_map_option unquote_variance) (unquote_list v)) + (fun v -> [||], CArray.map_of_list (unquote_map_option unquote_variance) (unquote_list v)) variance in let priv = unquote_map_option unquote_bool priv in From aefa05303a700e235f61b0a558470a63da5f4d5d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 19 Mar 2026 00:34:00 +0000 Subject: [PATCH 2/2] Fix ast_quoter: mind_entry_variance is MetaRocq AST type, not Rocq kernel entry This file constructs Ast0.mutual_inductive_entry (where mind_entry_variance is Variance.t option list option), not Entries.mutual_inductive_entry. The tuple wrapping is incorrect here. Co-Authored-By: Claude Opus 4.6 (1M context) --- template-rocq/src/ast_quoter.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/template-rocq/src/ast_quoter.ml b/template-rocq/src/ast_quoter.ml index 074496aa7..e4f337f41 100644 --- a/template-rocq/src/ast_quoter.ml +++ b/template-rocq/src/ast_quoter.ml @@ -355,7 +355,7 @@ struct mind_entry_inds = List.map quote_one_inductive_entry is; mind_entry_template = false; mind_entry_universes = univs; - mind_entry_variance = Option.map (fun v -> [||], v) variance; + mind_entry_variance = variance; mind_entry_private = None } let quote_definition_entry ty body ctx =