Document changes

4 files changed, 66 insertions, 32 deletions

diff --git a/engine/evd.mli b/engine/evd.mli
index 89dcd92ce..86887f3dc 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -467,7 +467,17 @@ val retract_coercible_metas : evar_map -> metabinding list * evar_map
 (*********************************************************
    Sort/universe variables *)
 
-(** Rigid or flexible universe variables *)
+(** Rigid or flexible universe variables.
+
+   [UnivRigid] variables are user-provided or come from an explicit
+   [Type] in the source, we do not minimize them or unify them eagerly.
+
+   [UnivFlexible alg] variables are fresh universe variables of
+   polymorphic constants or generated during refinement, sometimes in
+   algebraic position (i.e. not appearing in the term at the moment of
+   creation). They are the candidates for minimization (if alg, to an
+   algebraic universe) and unified eagerly in the first-order
+   unification heurstic.  *)
 
 type rigid = UState.rigid =
   | UnivRigid
diff --git a/kernel/univ.ml b/kernel/univ.ml
index c863fac0e..09f884ecd 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -468,20 +468,32 @@ struct
       else if Level.is_prop u then
 	hcons (Level.set,n+k)
       else hcons (u,n+k)
-	
+
+    type super_result =
+	SuperSame of bool
+        (* The level expressions are in cumulativity relation. boolean
+           indicates if left is smaller than right?  *)
+      | SuperDiff of int
+        (* The level expressions are unrelated, the comparison result
+           is canonical *)
+
+    (** [super u v] compares two level expressions,
+       returning [SuperSame] if they refer to the same level at potentially different
+       increments or [SuperDiff] if they are different. The booleans indicate if the
+       left expression is "smaller" than the right one in both cases. *)
     let super (u,n as x) (v,n' as y) =
       let cmp = Level.compare u v in
-	if Int.equal cmp 0 then Inl (n < n')
+	if Int.equal cmp 0 then SuperSame (n < n')
 	else
 	  match x, y with
 	  | (l,0), (l',0) ->
 	     let open RawLevel in
 	     (match Level.data l, Level.data l' with
-	      | Prop, Prop -> Inl false
-	      | Prop, _ -> Inl true
-	      | _, Prop -> Inl false
-	      | _, _ -> Inr cmp)
-	  | _, _ -> Inr cmp
+	      | Prop, Prop -> SuperSame false
+	      | Prop, _ -> SuperSame true
+	      | _, Prop -> SuperSame false
+	      | _, _ -> SuperDiff cmp)
+	  | _, _ -> SuperDiff cmp
 
     let to_string (v, n) =
       if Int.equal n 0 then Level.to_string v
@@ -603,24 +615,26 @@ struct
     | Nil, _ -> l2
     | _, Nil -> l1
     | Cons (h1, _, t1), Cons (h2, _, t2) ->
-      (match Expr.super h1 h2 with
-      | Inl true (* h1 < h2 *) -> merge_univs t1 l2
-      | Inl false -> merge_univs l1 t2
-      | Inr c -> 
-        if c <= 0 (* h1 < h2 is name order *)
-	then cons h1 (merge_univs t1 l2)
-	else cons h2 (merge_univs l1 t2))
+       let open Expr in
+       (match super h1 h2 with
+	| SuperSame true (* h1 < h2 *) -> merge_univs t1 l2
+	| SuperSame false -> merge_univs l1 t2
+	| SuperDiff c ->
+           if c <= 0 (* h1 < h2 is name order *)
+	   then cons h1 (merge_univs t1 l2)
+	   else cons h2 (merge_univs l1 t2))
 
   let sort u =
     let rec aux a l = 
       match l with
       | Cons (b, _, l') ->
-        (match Expr.super a b with
-	| Inl false -> aux a l'
-	| Inl true -> l
-	| Inr c ->
-	  if c <= 0 then cons a l
-	  else cons b (aux a l'))
+	let open Expr in
+        (match super a b with
+	 | SuperSame false -> aux a l'
+	 | SuperSame true -> l
+	 | SuperDiff c ->
+	    if c <= 0 then cons a l
+	    else cons b (aux a l'))
       | Nil -> cons a l
     in 
       fold (fun a acc -> aux a acc) u nil
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 27c1dd031..6e4d72705 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1935,6 +1935,9 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
 
 let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
   let refresh_tycon sigma t =
+    (** If we put the typing constraint in the term, it has to be
+       refreshed to preserve the invariant that no algebraic universe
+       can appear in the term.  *)
     refresh_universes ~status:Evd.univ_flexible ~onlyalg:true (Some true)
 		      env sigma t
   in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 02e10d7fc..4fd030845 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -46,30 +46,35 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
 		      pbty env evd t =
   let evdref = ref evd in
   let modified = ref false in
-  let refresh_sort status dir s =
+  (* direction: true for fresh universes lower than the existing ones *)
+  let refresh_sort status ~direction s =
     let s' = evd_comb0 (new_sort_variable status) evdref in
     let evd = 
-      if dir then set_leq_sort env !evdref s' s
+      if direction then set_leq_sort env !evdref s' s
       else set_leq_sort env !evdref s s'
     in
     modified := true; evdref := evd; mkSort s'
   in
-  let rec refresh onlyalg status dir t = 
+  let rec refresh ~onlyalg status ~direction t =
     match kind_of_term t with
     | Sort (Type u as s) ->
        (match Univ.universe_level u with
-	| None -> refresh_sort status dir s
+	| None -> refresh_sort status ~direction s
 	| Some l ->
 	   (match Evd.universe_rigidity evd l with
-	    | UnivRigid -> if not onlyalg then refresh_sort status dir s else t
+	    | UnivRigid ->
+	       if not onlyalg then refresh_sort status ~direction s
+	       else t
 	    | UnivFlexible alg ->
 	       if onlyalg && alg then
 	         (evdref := Evd.make_flexible_variable !evdref false l; t)
 	       else t))
-    | Sort (Prop Pos as s) when refreshset && not dir ->
-       refresh_sort status dir s
+    | Sort (Prop Pos as s) when refreshset && not direction ->
+       (* Cannot make a universe "lower" than "Set",
+          only refreshing when we want higher universes. *)
+       refresh_sort status ~direction s
     | Prod (na,u,v) -> 
-      mkProd (na, u, refresh onlyalg status dir v)
+      mkProd (na, u, refresh ~onlyalg status ~direction v)
     | _ -> t
   (** Refresh the types of evars under template polymorphic references *)
   and refresh_term_evars onevars top t =
@@ -82,7 +87,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
       Array.iter (refresh_term_evars onevars false) args
     | Evar (ev, a) when onevars ->
       let evi = Evd.find !evdref ev in
-      let ty' = refresh onlyalg univ_flexible true evi.evar_concl in
+      let ty' = refresh ~onlyalg univ_flexible ~direction:true evi.evar_concl in
 	if !modified then 
 	  evdref := Evd.add !evdref ev {evi with evar_concl = ty'}
 	else ()
@@ -103,8 +108,10 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
   let t' = 
     if isArity t then
       match pbty with
-      | None -> refresh true univ_flexible false t
-      | Some dir -> refresh onlyalg status dir t
+      | None ->
+	 (* No cumulativity needed, but we still need to refresh the algebraics *)
+	 refresh ~onlyalg:true univ_flexible ~direction:false t
+      | Some direction -> refresh ~onlyalg status ~direction t
     else (refresh_term_evars false true t; t)
   in
     if !modified then !evdref, t' else !evdref, t