Remove the uses of the dubious PConstraints.ContextSet.t type.

Author: ppedrot

src/rocq_elpi_HOAS.ml

@@ -211,7 +211,6 @@ let universe_level_variable =
 [%%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
 
 let univ_lt = Univ.Lt
 let univ_le = Univ.Le
@@ -253,7 +252,6 @@ let universe_constraint : univ_cst API.Conversion.t =
 [%%else]
 type univ_cst = Univ.UnivConstraint.t
 type univ_csts = Univ.UnivConstraints.t
-type univ_ctx_set = PConstraints.ContextSet.t
 let univ_lt = Univ.UnivConstraint.Lt
 let univ_le = Univ.UnivConstraint.Le
 let univ_eq = Univ.UnivConstraint.Eq

src/rocq_elpi_HOAS.mli

@@ -27,11 +27,9 @@ type uinstanceoption =
 [%%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
 [%%else]
 type univ_cst = Univ.UnivConstraint.t
 type univ_csts = Univ.UnivConstraints.t
-type univ_ctx_set = PConstraints.ContextSet.t
 [%%endif]
 
 type universe_decl = (Univ.Level.t list * bool) * (univ_csts * bool)

src/rocq_elpi_builtins.ml

@@ -355,15 +355,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 check_univ_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
 let default_polyflags = false
 [%%else]
 let evd_merge_sort_context_set rigid = Evd.merge_sort_context_set rigid QGraph.Internal
 let check_univ_decl =  UState.check_univ_decl
-let empty_ctxset = PConstraints.ContextSet.empty
 let univ_csts_to_list = Univ.UnivConstraints.elements
 let univs_of_csts x = PConstraints.univs @@ UState.constraints x
 let ucsts_filter = Univ.UnivConstraints.filter