Merge pull request #939 from ppedrot/reduce-pcontext-api

Adapt to rocq-prover/rocq#21394.

Author: SkySkimmer

src/rocq_elpi_HOAS.ml

@@ -1756,11 +1756,11 @@ let mk_global state gr inst_opt = S.update_return engine state (fun x ->
 ) |> (fun (x,(y,z)) -> x,y,z)
 
 [%%if coq = "9.0" || coq = "9.1"]
-let merge_universe_context_sext sigma uctx =
-  Evd.merge_context_set Evd.univ_rigid sigma uctx
+let merge_universe_context_set rigid sigma uctx =
+  Evd.merge_context_set rigid sigma uctx
 [%%else]
-let merge_universe_context_sext sigma uctx =
-  Evd.merge_context_set Evd.univ_rigid sigma (PConstraints.ContextSet.of_univ_context_set uctx)
+let merge_universe_context_set rigid sigma uctx =
+  Evd.merge_context_set rigid sigma (PConstraints.ContextSet.of_univ_context_set uctx)
 [%%endif]
 
 let body_of_constant state c inst_opt = S.update_return engine state (fun x ->
@@ -1776,7 +1776,7 @@ let body_of_constant state c inst_opt = S.update_return engine state (fun x ->
      | Opaqueproof.PrivateMonomorphic () -> sigma
      | Opaqueproof.PrivatePolymorphic ctx ->
       let ctx = Util.on_snd (subst_univs_constraints (snd (UVars.make_instance_subst inst))) ctx in
-      merge_universe_context_sext sigma ctx
+      merge_universe_context_set Evd.univ_rigid sigma ctx
      in
      { x with sigma }, (Some (EConstr.of_constr bo), Some inst)
   | None -> x, (None, None)) |> (fun (x,(y,z)) -> x,y,z)
@@ -3645,7 +3645,7 @@ let inductive_entry2lp ~depth coq_ctx constraints state ~loose_udecl e =
   let indno = 1 in
   let state = 
     S.update engine state (fun e ->
-      { e with sigma = Evd.merge_context_set UState.univ_flexible e.sigma uctx}) in
+      { e with sigma = merge_universe_context_set UState.univ_flexible e.sigma uctx}) in
   let state = match mie.mind_entry_universes with
     | Template_ind_entry _ -> nYI "template polymorphic inductives"
     | Monomorphic_ind_entry -> state
@@ -3768,7 +3768,7 @@ let record_entry2lp ~depth coq_ctx constraints state ~loose_udecl (decl:Record.R
 
   let state =
     S.update engine state (fun e ->
-        { e with sigma = Evd.merge_context_set UState.univ_flexible e.sigma decl.entry.global_univs})
+        { e with sigma = merge_universe_context_set UState.univ_flexible e.sigma decl.entry.global_univs})
   in
 
   let state = match mie.mind_entry_universes with

src/rocq_elpi_HOAS.mli

@@ -126,14 +126,10 @@ type record_field_spec = { name : Name.t; is_coercion : coercion_status; is_cano
 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
-[%%elif 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 * UState.named_universes_entry * (bool * record_field_spec list) option * DeclareInd.one_inductive_impls list) * Conversion.extra_goals
 [%%else]
 val lp2inductive_entry :
   depth:int -> empty coq_context -> constraints -> State.t -> term ->
-  State.t * (DeclareInd.default_dep_elim list * Entries.mutual_inductive_entry * PConstraints.ContextSet.t * UState.named_universes_entry * (bool * record_field_spec list) option * DeclareInd.one_inductive_impls list) * Conversion.extra_goals
+  State.t * (DeclareInd.default_dep_elim list * Entries.mutual_inductive_entry * Univ.ContextSet.t * UState.named_universes_entry * (bool * record_field_spec list) option * DeclareInd.one_inductive_impls list) * Conversion.extra_goals
 [%%endif]
 
 [%%if coq = "9.0"]

src/rocq_elpi_builtins.ml

@@ -354,17 +354,13 @@ let is_mutual_inductive_entry_ground { Entries.mind_entry_params; mind_entry_ind
 
 [%%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
 let empty_ctxset = Univ.ContextSet.empty
 let univ_csts_to_list = Univ.Constraints.elements
 let univs_of_csts = UState.constraints
 let ucsts_filter = Univ.Constraints.filter
 [%%else]
 let evd_merge_sort_context_set rigid = Evd.merge_sort_context_set rigid QGraph.Internal
-let global_push_context_set x =
-  let () = Global.push_context_set (PConstraints.ContextSet.univ_context_set x) in
-  Global.push_qualities QGraph.Internal (PConstraints.ContextSet.sort_context_set x)
 let check_sort_poly_decl =  UState.check_sort_poly_decl
 let empty_ctxset = PConstraints.ContextSet.empty
 let univ_csts_to_list = Univ.UnivConstraints.elements
@@ -987,17 +983,13 @@ let eval_to_oeval = Evaluable.to_kevaluable
 let mkCLocalAssum x y z = Constrexpr.CLocalAssum(x,None,y,z)
 let pattern_of_glob_constr env g = Patternops.pattern_of_glob_constr env g
 
-[%%if coq = "9.0" || coq = "9.1"]
 let get_entry_context = function
 | UState.Monomorphic_entry x, _ -> x
 | _ -> Univ.ContextSet.empty
 
+[%%if coq = "9.0" || coq = "9.1"]
 let drop_sort_context uctx = uctx
 [%%else]
-let get_entry_context = function
-| UState.Monomorphic_entry x, _ -> PConstraints.ContextSet.univ_context_set x
-| _ -> Univ.ContextSet.empty
-
 let drop_sort_context = PConstraints.ContextSet.univ_context_set
 [%%endif]
 
@@ -2361,7 +2353,7 @@ Supported attributes:
        | Polymorphic_ind_entry uctx ->
           (Polymorphic_entry uctx, UState.Polymorphic_entry uctx, univ_binders)
        in
-     let () = global_push_context_set uctx in
+     let () = Global.push_context_set uctx in
      let mind =
        let univ_binders = univ_binder_compat_820 (uentry', ubinders) univ_binders in
        declare_mutual_inductive_with_eliminations ~primitive_expected ~default_dep_elim me univ_binders ind_impls in
@@ -2396,7 +2388,6 @@ Supported attributes:
            | Names.Name id -> Dumpglob.dump_definition (lid_of id) false "proj"
            | Names.Anonymous -> ()) names;
       end;
-      let uctx = drop_sort_context uctx in (* ??? *)
       uctx,state, !: ind, []))),
   DocAbove);