Univs: fix bug #3807

Add a flag to disallow minimization to set

6 files changed, 27 insertions, 3 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 34eb283d7..c0bd3bacd 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1797,6 +1797,9 @@ struct
   let empty = (LSet.empty, Constraint.empty)
   let is_empty (univs, cst) = LSet.is_empty univs && Constraint.is_empty cst
 
+  let equal (univs, cst as x) (univs', cst' as y) =
+    x == y || (LSet.equal univs univs' && Constraint.equal cst cst')
+									
   let of_set s = (s, Constraint.empty)
   let singleton l = of_set (LSet.singleton l)
   let of_instance i = of_set (Instance.levels i)
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 4cc8a2528..cbaf7e546 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -360,6 +360,7 @@ sig
   val of_instance : Instance.t -> t
   val of_set : universe_set -> t
 
+  val equal : t -> t -> bool
   val union : t -> t -> t
 
   val append : t -> t -> t
diff --git a/library/universes.ml b/library/universes.ml
index bc42cc044..0656188eb 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -26,6 +26,11 @@ let pr_with_global_universes l =
   try Nameops.pr_id (LMap.find l (snd !global_universes))
   with Not_found -> Level.pr l
 
+(* To disallow minimization to Set *)
+
+let set_minimization = ref true
+let is_set_minimization () = !set_minimization
+			    
 type universe_constraint_type = ULe | UEq | ULub
 
 type universe_constraint = universe * universe_constraint_type * universe
@@ -832,7 +837,9 @@ let normalize_context_set ctx us algs =
     Constraint.fold (fun (l,d,r as cstr) (smallles, noneqs) ->
         if d == Le then
 	  if Univ.Level.is_small l then
-	    (Constraint.add cstr smallles, noneqs)
+	    if is_set_minimization () then
+	      (Constraint.add cstr smallles, noneqs)
+	    else (smallles, noneqs)
 	  else if Level.is_small r then
 	    if Level.is_prop r then
 	      raise (Univ.UniverseInconsistency
@@ -872,6 +879,8 @@ let normalize_context_set ctx us algs =
       if d == Eq then (UF.union l r uf; noneqs)
       else (* We ignore the trivial Prop/Set <= i constraints. *)
 	if d == Le && Univ.Level.is_small l then noneqs
+	else if Univ.Level.is_prop l && d == Lt && Univ.Level.is_set r
+	then noneqs
 	else Constraint.add cstr noneqs)
       csts Constraint.empty
   in
diff --git a/library/universes.mli b/library/universes.mli
index 5527da090..4ff21d45c 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -12,6 +12,9 @@ open Term
 open Environ
 open Univ
 
+val set_minimization : bool ref
+val is_set_minimization : unit -> bool
+       
 (** Universes *)
 
 type universe_names = 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 412fb92b3..3d912ca4c 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1324,8 +1324,7 @@ let normalize_evar_universe_context uctx =
       Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables
         uctx.uctx_univ_algebraic
     in
-      if Univ.LSet.equal (fst us') (fst uctx.uctx_local) then 
-        uctx
+      if Univ.ContextSet.equal us' uctx.uctx_local then uctx
       else
 	let us', universes = Universes.refresh_constraints uctx.uctx_initial_universes us' in
 	let uctx' = 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index dec23328f..6306739b7 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -112,6 +112,15 @@ let _ =
 	    optkey   = ["Strict";"Universe";"Declaration"];
 	    optread  = is_strict_universe_declarations;
 	    optwrite = (:=) strict_universe_declarations })
+
+let _ =
+  Goptions.(declare_bool_option
+	  { optsync  = true;
+            optdepr  = false;
+	    optname  = "minimization to Set";
+	    optkey   = ["Universe";"set";"Minimization"];
+	    optread  = Universes.is_set_minimization;
+	    optwrite = (:=) Universes.set_minimization })
 						  
 (** Miscellaneous interpretation functions *)
 let interp_universe_level_name evd (loc,s) =