Merge pull request MetaRocq#1229 from ppedrot/rm-pconstraints-contextset

Stop using the dubious Rocq type PConstraints.ContextSet.t.

Author: ppedrot

template-rocq/src/ast_quoter.ml

@@ -196,10 +196,10 @@ struct
     let constraints = UVars.UContext.constraints uctx in
     (names, (quote_univ_instance levels, quote_univ_constraints (PConstraints.univs constraints)))
 
-  let quote_contextset (uctx : PConstraints.ContextSet.t) : quoted_contextset =
-    let levels = List.map quote_level (Univ.Level.Set.elements (PConstraints.ContextSet.levels uctx)) in
-    let constraints = PConstraints.ContextSet.constraints uctx in
-    (Universes0.LevelSetProp.of_list levels, quote_univ_constraints (PConstraints.univs constraints))
+  let quote_contextset (uctx : Univ.ContextSet.t) : quoted_contextset =
+    let levels = List.map quote_level (Univ.Level.Set.elements (Univ.ContextSet.levels uctx)) in
+    let constraints = Univ.ContextSet.constraints uctx in
+    (Universes0.LevelSetProp.of_list levels, quote_univ_constraints constraints)
 
   let quote_abstract_univ_context uctx : quoted_abstract_univ_context =
     let {UVars.quals = qnames; UVars.univs = unames} = UVars.AbstractContext.names uctx in

template-rocq/src/constr_quoter.ml

@@ -277,8 +277,8 @@ struct
     to_coq_list (Lazy.force tVariance) var_list
 
   let quote_contextset uctx =
-    let levels' = quote_levelset (PConstraints.ContextSet.levels uctx) in
-    let const' = quote_univ_constraints (PConstraints.ContextSet.univ_constraints uctx) in
+    let levels' = quote_levelset (Univ.ContextSet.levels uctx) in
+    let const' = quote_univ_constraints (Univ.ContextSet.constraints uctx) in
     pairl tLevelSet tConstraintSet levels' const'
 
   let quote_univ_context uctx =

template-rocq/src/quoter.ml

@@ -113,7 +113,7 @@ sig
   val quote_univ_instance : UVars.Instance.t -> quoted_univ_instance
   val quote_univ_constraints : Univ.UnivConstraints.t -> quoted_univ_constraints
   val quote_univ_context : UVars.UContext.t -> quoted_univ_context
-  val quote_contextset : PConstraints.ContextSet.t -> quoted_contextset
+  val quote_contextset : Univ.ContextSet.t -> quoted_contextset
   val quote_variance : UVars.Variance.t -> quoted_variance
   val quote_abstract_univ_context : UVars.AbstractContext.t -> quoted_abstract_univ_context
 
@@ -231,8 +231,7 @@ struct
         eqs (levels, cstrs)
     in
     let levels = Univ.Level.Set.add Univ.Level.set levels in
-    let cstrs = PConstraints.of_univs cstrs in
-    debug Pp.(fun () -> str"Universe context: " ++ PConstraints.ContextSet.pr Sorts.QVar.raw_pr Univ.Level.raw_pr (levels, cstrs));
+    debug Pp.(fun () -> str"Universe context: " ++ Univ.ContextSet.pr Univ.Level.raw_pr (levels, cstrs));
     time (Pp.str"Quoting universe context")
       (fun uctx -> Q.quote_contextset uctx) (levels, cstrs)
 
@@ -605,7 +604,7 @@ struct
       else
         (debug Pp.(fun () -> str"Skipping universes: ");
          time (Pp.str"Quoting empty universe context")
-           (fun uctx -> Q.quote_contextset uctx) PConstraints.ContextSet.empty)
+           (fun uctx -> Q.quote_contextset uctx) Univ.ContextSet.empty)
     in
     let retro =
       let retro = Environ.retroknowledge env in