Fix overlay for elimination-constraints

Author: mattam82

src/rocq_elpi_HOAS.ml

@@ -108,7 +108,7 @@ let constraint_eq u1 u2 =
   let open UnivProblem in
   ULe (u1, u2)
 
-[%%if coq = "9.0" || coq = "9.1" || coq = "9.2"]
+[%%if coq = "9.0" || coq = "9.1"]
 let add_constraints state c = S.update (Option.get !pre_engine) state (fun ({ sigma } as x) ->
   { x with sigma = Evd.add_universe_constraints sigma c })
 [%%else]
@@ -208,7 +208,7 @@ let universe_level_variable =
   end
 }
 
-[%%if coq = "9.0" || coq = "9.1" || coq = "9.2"]
+[%%if coq = "9.0" || coq = "9.1"]
 type univ_cst = Univ.univ_constraint
 type univ_csts = Univ.Constraints.t
 type univ_ctx_set = Univ.ContextSet.t
@@ -261,7 +261,7 @@ let univ_eq = Univ.UnivConstraint.Eq
 let univ_csts_of_list = Univ.UnivConstraints.of_list
 let univ_csts_to_list = Univ.UnivConstraints.elements
 let evd_merge_ctx_set rigid = Evd.merge_sort_context_set rigid QGraph.Internal
-let subst_univs_constraints x = UVars.subst_univ_constraints (Sorts.QVar.Map.empty,x)
+let subst_univs_constraints x = UVars.subst_univs_constraints (Sorts.QVar.Map.empty,x)
 let univs_of_csts x = PConstraints.univs @@ UVars.UContext.constraints x
 let mk_universe_decl sort_poly_decl_extensible_instance sort_poly_decl_extensible_constraints sort_poly_decl_univ_constraints sort_poly_decl_instance =
   let open UState in

src/rocq_elpi_HOAS.mli

@@ -24,7 +24,7 @@ type uinstanceoption =
   | VarInstance of (FlexibleData.Elpi.t * RawData.term list * inv_rel_key)
     (* a variable was provided, the command will compute the instance to unify with it *)
 
-[%%if coq = "9.0" || coq = "9.1" || coq = "9.2"]
+[%%if coq = "9.0" || coq = "9.1"]
 type univ_cst = Univ.univ_constraint
 type univ_csts = Univ.Constraints.t
 type univ_ctx_set = Univ.ContextSet.t
@@ -122,7 +122,7 @@ val lp2skeleton :
 type coercion_status = Regular | Off | Reversible
 type record_field_spec = { name : Name.t; is_coercion : coercion_status; is_canonical : bool }
 
-[%%if coq = "9.0" || coq = "9.1" || coq = "9.2"]
+[%%if coq = "9.0" || coq = "9.1"]
 val lp2inductive_entry :
   depth:int -> empty coq_context -> constraints -> State.t -> term ->
   State.t * (DeclareInd.default_dep_elim list * Entries.mutual_inductive_entry * Univ.ContextSet.t * UnivNames.universe_binders * (bool * record_field_spec list) option * DeclareInd.one_inductive_impls list) * Conversion.extra_goals
@@ -233,7 +233,7 @@ val in_elpiast_primitive : loc:Ast.Loc.t -> primitive_value -> Ast.Term.t
 
 val uinstance : UVars.Instance.t Conversion.t
 
-[%%if coq = "9.0" || coq = "9.1" || coq = "9.2"]
+[%%if coq = "9.0" || coq = "9.1"]
 val universe_constraint : Univ.univ_constraint Conversion.t
 [%%else]
 val universe_constraint : Univ.UnivConstraint.t Conversion.t
@@ -325,7 +325,7 @@ val body_of_constant :
 val grab_global_env_drop_univs_and_sigma : State.t -> State.t
 val grab_global_env_drop_sigma : State.t -> State.t
 
-[%%if coq = "9.0" || coq = "9.1" || coq = "9.2"]
+[%%if coq = "9.0" || coq = "9.1"]
 val grab_global_env : uctx:Univ.ContextSet.t -> State.t -> State.t
 val grab_global_env_drop_sigma_keep_univs : uctx:Univ.ContextSet.t -> State.t -> State.t
 [%%else]
@@ -372,7 +372,7 @@ val merge_universe_context : state -> UState.t -> state
 val restricted_sigma_of : Univ.Level.Set.t -> state -> Evd.evar_map
 val universes_of_term : state -> EConstr.t -> Univ.Level.Set.t
 
-[%%if coq = "9.0" || coq = "9.1" || coq = "9.2"]
+[%%if coq = "9.0" || coq = "9.1"]
 val poly_cumul_udecl_variance_of_options : state -> options -> state * bool * bool * UState.universe_decl * Entries.variance_entry
 val universes_of_udecl : state -> UState.universe_decl -> Univ.Level.Set.t
 [%%else]

src/rocq_elpi_arg_HOAS.ml

@@ -138,7 +138,7 @@ type raw_red_expr = Genredexpr.raw_red_expr
 type raw_red_expr = Redexpr.raw_red_expr
 [%%endif]
 
-[%%if coq = "9.0" || coq = "9.1" || coq = "9.2"]
+[%%if coq = "9.0" || coq = "9.1"]
 type raw_constant_decl = {
   name : qualified_name;
   atts : Attributes.vernac_flags;

src/rocq_elpi_arg_HOAS.mli

@@ -30,7 +30,7 @@ type raw_red_expr = Genredexpr.raw_red_expr
 type raw_red_expr = Redexpr.raw_red_expr
 [%%endif]
 
-[%%if coq = "9.0" || coq = "9.1" || coq = "9.2"]
+[%%if coq = "9.0" || coq = "9.1"]
 type raw_constant_decl = {
   name : qualified_name;
   atts : Attributes.vernac_flags;

src/rocq_elpi_arg_syntax.mlg

@@ -42,7 +42,7 @@ let streamOk x = Ok x
 let streamFail () = Error ()
 [%%endif]
 
-[%%if coq = "9.0" || coq = "9.1" || coq = "9.2"]
+[%%if coq = "9.0" || coq = "9.1"]
 let sort_poly_decl = Procq.Prim.univ_decl
 [%%else]
 let sort_poly_decl = Procq.Prim.sort_poly_decl

src/rocq_elpi_builtins.ml

@@ -352,7 +352,7 @@ let is_mutual_inductive_entry_ground { Entries.mind_entry_params; mind_entry_ind
   List.for_all (is_ground_rel_ctx_entry sigma) mind_entry_params &&
   List.for_all (is_ground_one_inductive_entry sigma) mind_entry_inds
 
-[%%if coq = "9.0" || coq = "9.1" || coq = "9.2"]
+[%%if coq = "9.0" || coq = "9.1"]
 let evd_merge_sort_context_set rigid = Evd.merge_sort_context_set rigid
 let global_push_context_set x = Global.push_context_set x
 let check_sort_poly_decl =  UState.check_univ_decl