collapse_sort_variables rename and flip to_type argument to only_above_prop and make it non implicit

dev/ci/user-overlays/21820-SkySkimmer-only-above.sh

@@ -0,0 +1,9 @@
+overlay elpi https://github.com/SkySkimmer/coq-elpi only-above 21820
+
+overlay equations https://github.com/SkySkimmer/Coq-Equations only-above 21820
+
+overlay mtac2 https://github.com/SkySkimmer/Mtac2 only-above 21820
+
+overlay rewriter https://github.com/SkySkimmer/rewriter only-above 21820
+
+overlay waterproof https://github.com/SkySkimmer/coq-waterproof only-above 21820

engine/evd.ml

@@ -1040,7 +1040,7 @@ let check_univ_decl_early ~poly ~with_obls sigma udecl terms =
   in
   let vars = List.fold_left (fun acc b -> Univ.Level.Set.union acc (Vars.universes_of_constr b)) Univ.Level.Set.empty terms in
   let uctx = ustate sigma in
-  let uctx = UState.collapse_sort_variables ~to_type:(PolyFlags.collapse_sort_variables poly) uctx in
+  let uctx = UState.collapse_sort_variables ~only_above_prop:(not @@ PolyFlags.collapse_sort_variables poly) uctx in
   let uctx = UState.restrict uctx vars in
   ignore (UState.check_univ_decl ~poly uctx udecl)
 
@@ -1222,8 +1222,8 @@ let nf_univ_variables evd =
   let uctx = UState.normalize_variables evd.universes in
   {evd with universes = uctx}
 
-let collapse_sort_variables ?except ?(to_type = true) evd =
-  let universes = UState.collapse_sort_variables ?except ~to_type evd.universes in
+let collapse_sort_variables ?except ~only_above_prop evd =
+  let universes = UState.collapse_sort_variables ?except ~only_above_prop evd.universes in
   { evd with universes }
 
 let minimize_universes_no_collapse evd =
@@ -1234,7 +1234,7 @@ let minimize_universes_no_collapse evd =
 let minimize_universes ?(poly=PolyFlags.default) evd =
   let collapse_sort_variables = PolyFlags.collapse_sort_variables poly in
   let uctx' =
-    UState.collapse_sort_variables ~to_type:collapse_sort_variables evd.universes
+    UState.collapse_sort_variables ~only_above_prop:(not collapse_sort_variables) evd.universes
   in
   minimize_universes_no_collapse {evd with universes = uctx'}
 

engine/evd.mli

@@ -659,7 +659,7 @@ val with_sort_context_set : ?loc:Loc.t -> ?sort_rigid:bool -> ?src:UState.constr
 
 val nf_univ_variables : evar_map -> evar_map
 
-val collapse_sort_variables : ?except:Sorts.QVar.Set.t -> ?to_type:bool -> evar_map -> evar_map
+val collapse_sort_variables : ?except:Sorts.QVar.Set.t -> only_above_prop:bool -> evar_map -> evar_map
 
 val fix_undefined_variables : evar_map -> evar_map
 

engine/uState.ml

@@ -101,7 +101,7 @@ module QState : sig
   val unify_quality : fail:(unit -> t) -> Conversion.conv_pb -> Quality.t -> Quality.t -> t -> t
   val undefined : t -> QVar.Set.t
   val collapse_above_prop : to_prop:bool -> t -> t
-  val collapse : ?except:QVar.Set.t -> ?to_type:bool -> t -> t
+  val collapse : ?except:QVar.Set.t -> only_above_prop:bool -> t -> t
   val pr : Sorts.Quality.printer -> (QVar.t -> Id.t option) -> t -> Pp.t
   val of_elims : QGraph.t -> t
   val elims : t -> QGraph.t
@@ -324,7 +324,7 @@ let collapse_above_prop ~to_prop m =
          )
          m.qmap m
 
-let collapse ?(except=QSet.empty) ?(to_type = true) m =
+let collapse ?(except=QSet.empty) ~only_above_prop m =
   let free_qualities = QMap.fold (fun q v fqs ->
       match v with
       | Equiv _ -> fqs
@@ -356,7 +356,7 @@ let collapse ?(except=QSet.empty) ?(to_type = true) m =
           if QSet.exists (fun q' -> dominates_above_prop q' q) free_qualities then
             Option.get (set q qprop m)
           else Option.get (set q qtype m)
-        else if to_type then Option.get (set q qtype m) else m)
+        else if not only_above_prop then Option.get (set q qtype m) else m)
     m.qmap m
 
 let pr prqvar local_name ({ qmap; elims } as m) =
@@ -1561,8 +1561,8 @@ let collapse_above_prop_sort_variables ~to_prop uctx =
   let sorts = QState.collapse_above_prop ~to_prop uctx.sort_variables in
   normalize_quality_variables { uctx with sort_variables = sorts }
 
-let collapse_sort_variables ?except ?(to_type = true) uctx =
-  let sorts = QState.collapse ?except ~to_type uctx.sort_variables in
+let collapse_sort_variables ?except ~only_above_prop uctx =
+  let sorts = QState.collapse ?except ~only_above_prop uctx.sort_variables in
   normalize_quality_variables { uctx with sort_variables = sorts }
 
 let minimize uctx =

engine/uState.mli

@@ -240,7 +240,7 @@ val minimize : t -> t
 
 val collapse_above_prop_sort_variables : to_prop:bool -> t -> t
 
-val collapse_sort_variables : ?except:QVar.Set.t -> ?to_type:bool -> t -> t
+val collapse_sort_variables : ?except:QVar.Set.t -> only_above_prop:bool -> t -> t
 
 type ('a, 'b, 'c, 'd) gen_universe_decl = {
   univdecl_qualities : 'a;

vernac/comInductive.ml

@@ -524,7 +524,7 @@ type should_template =
   | NotTemplate
 
 let nontemplate_univ_entry ~poly sigma udecl =
-  let sigma = Evd.collapse_sort_variables ~to_type:(PolyFlags.collapse_sort_variables poly) sigma in
+  let sigma = Evd.collapse_sort_variables ~only_above_prop:(not @@ PolyFlags.collapse_sort_variables poly) sigma in
   let uentry, _ as ubinders = Evd.check_univ_decl ~poly sigma udecl in
   let uentry, global = match uentry with
     | UState.Polymorphic_entry uctx -> Polymorphic_ind_entry uctx, Univ.ContextSet.empty
@@ -537,7 +537,7 @@ let template_univ_entry sigma udecl ~template_univs pseudo_sort_poly =
     | Some q -> QVar.Set.singleton q
     | None -> QVar.Set.empty
   in
-  let sigma = Evd.collapse_sort_variables ~except:template_qvars sigma in
+  let sigma = Evd.collapse_sort_variables ~except:template_qvars ~only_above_prop:false sigma in
   let sigma = QVar.Set.fold (fun q sigma -> Evd.set_above_prop sigma (QVar q))
       template_qvars sigma
   in

vernac/declare.ml

@@ -1212,7 +1212,7 @@ module ProgramDecl = struct
       if PolyFlags.univ_poly poly then uctx
       else
         (* declare global univs of the main constant before we do obligations *)
-        let uctx = UState.collapse_sort_variables ~to_type:(PolyFlags.collapse_sort_variables poly) uctx in
+        let uctx = UState.collapse_sort_variables ~only_above_prop:(not @@ PolyFlags.collapse_sort_variables poly) uctx in
         let ctx = UState.check_mono_sort_constraints uctx in
         let () = Global.push_context_set ctx in
         let cst = Constant.make2 (Lib.current_mp()) cinfo.CInfo.name in

vernac/vernacentries.ml

@@ -2164,7 +2164,7 @@ let vernac_global_check c =
   let sigma = Evd.from_env env in
   let c = Constrintern.intern_constr env sigma c in
   let sigma, c = Pretyping.understand_tcc ~flags:Pretyping.all_and_fail_flags env sigma c in
-  let sigma = Evd.collapse_sort_variables sigma in
+  let sigma = Evd.collapse_sort_variables ~only_above_prop:false sigma in
   let c = EConstr.to_constr sigma c in
   let (qs, us), (qcst, ucst) as uctx = Evd.sort_context_set sigma in
    (* always empty due to collapse *)