Skip to content

Adapt to rocq-prover/rocq#21773 (sort poly cumulativity) #1250

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
SkySkimmer wants to merge 2 commits into
base: main
Choose a base branch
from
+8 −2
Draft

Adapt to rocq-prover/rocq#21773 (sort poly cumulativity) #1250

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
2ece985
Adapt to rocq-prover/rocq#21773 (sort poly cumulativity)
SkySkimmer Mar 18, 2026
aefa053
Fix ast_quoter: mind_entry_variance is MetaRocq AST type, not Rocq ke…
JasonGross Mar 19, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 7 additions & 1 deletion template-rocq/src/quoter.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand Down
2 changes: 1 addition & 1 deletion template-rocq/src/run_template_monad.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading