From dd3d1fe92a14036996140b9dfdc6f73068ebc490 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 24 Feb 2025 13:38:38 +0100 Subject: [PATCH] Adapt to coq/coq#20272 (declare_axiom takes loc) --- src/rocq_elpi_builtins.ml | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/src/rocq_elpi_builtins.ml b/src/rocq_elpi_builtins.ml index 398428698..7ceb691ec 100644 --- a/src/rocq_elpi_builtins.ml +++ b/src/rocq_elpi_builtins.ml @@ -860,14 +860,16 @@ let warn_deprecated_add_axiom = "section variables is deprecated. Use coq.env.add-axiom or " ^ "coq.env.add-section-variable instead")) -let comAssumption_declare_variable id coe ~kind ty ~univs ~impargs impl ~name:_ = - ComAssumption.declare_variable ~coe ~kind ty ~univs ~impargs ~impl ~name:id -let comAssumption_declare_axiom coe ~local ~kind ~univs ~impargs ~inline ~name:_ ~id ty = - ComAssumption.declare_axiom ~coe ~local ~kind ~univs ~impargs ~inline ~name:id ty +let comAssumption_declare_variable coe ~kind ty ~univs ~impargs impl ~name = + ComAssumption.declare_variable ~coe ~kind ty ~univs ~impargs ~impl ~name:name.CAst.v [%%if coq = "8.20" || coq = "9.0"] +let comAssumption_declare_axiom coe ~local ~kind ~univs ~impargs ~inline ~name ty = + ComAssumption.declare_axiom ~coe ~local ~kind ~univs ~impargs ~inline ~name:name.CAst.v ty let declare_mutual_inductive_with_eliminations ~primitive_expected ~default_dep_elim x y z = DeclareInd.declare_mutual_inductive_with_eliminations ~primitive_expected ~default_dep_elim x y z [%%else] +let comAssumption_declare_axiom coe ~local ~kind ~univs ~impargs ~inline ~name ty = + ComAssumption.declare_axiom ~coe ~local ~kind ~univs ~impargs ~inline ~name ty let declare_mutual_inductive_with_eliminations ~primitive_expected ~default_dep_elim x y z = DeclareInd.declare_mutual_inductive_with_eliminations ~default_dep_elim x y z [%%endif] @@ -922,12 +924,12 @@ let add_axiom_or_variable api id ty local_bkind options state = match local_bkind with | Some implicit_kind -> begin Dumpglob.dump_definition name true "var"; - comAssumption_declare_variable id Vernacexpr.NoCoercion ~kind (EConstr.to_constr sigma ty) ~univs ~impargs implicit_kind ~name + comAssumption_declare_variable Vernacexpr.NoCoercion ~kind (EConstr.to_constr sigma ty) ~univs ~impargs implicit_kind ~name end | None -> begin Dumpglob.dump_definition name false "ax"; comAssumption_declare_axiom Vernacexpr.NoCoercion ~local:Locality.ImportDefaultBehavior ~kind (EConstr.to_constr sigma ty) - ~univs ~impargs ~inline:options.inline ~name ~id + ~univs ~impargs ~inline:options.inline ~name end in let ucsts = match univs with UState.Monomorphic_entry x, _ -> x | _ -> Univ.ContextSet.empty in