Remove unneeded fixpoint in normalize_context_set. Note that it is no

longer stable w.r.t. equality constraints as the universe graph will
choose different canonical levels depending on the equalities given to
it (l = r vs r = l).

3 files changed, 21 insertions, 45 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 00a869fda..425b67e08 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -275,9 +275,6 @@ let add_universe_constraints_context = UState.add_universe_constraints
 let constrain_variables = UState.constrain_variables 
 let evar_universe_context_of_binders = UState.of_binders
 
-(* let addunivconstrkey = Profile.declare_profile "add_universe_constraints_context";; *)
-(* let add_universe_constraints_context =  *)
-(*   Profile.profile2 addunivconstrkey add_universe_constraints_context;; *)
 (*******************************************************************)
 (* Metamaps *)
 
@@ -860,12 +857,9 @@ let set_eq_sort env d s1 s2 =
       d
 
 let has_lub evd u1 u2 =
-  (* let normalize = Universes.normalize_universe_opt_subst (ref univs.uctx_univ_variables) in *)
-  (* (\* let dref, norm = memo_normalize_universe d in *\) *)
-  (* let u1 = normalize u1 and u2 = normalize u2 in *)
-    if Univ.Universe.equal u1 u2 then evd
-    else add_universe_constraints evd
-      (Universes.Constraints.singleton (u1,Universes.ULub,u2))
+  if Univ.Universe.equal u1 u2 then evd
+  else add_universe_constraints evd
+    (Universes.Constraints.singleton (u1,Universes.ULub,u2))
 
 let set_eq_level d u1 u2 =
   add_constraints d (Univ.enforce_eq_level u1 u2 Univ.Constraint.empty)
@@ -883,15 +877,9 @@ let set_leq_sort env evd s1 s2 =
   match is_eq_sort s1 s2 with
   | None -> evd
   | Some (u1, u2) ->
-    (* if Univ.is_type0_univ u2 then *)
-    (*   if Univ.is_small_univ u1 then evd *)
-    (*   else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])) *)
-    (* else if Univ.is_type0m_univ u2 then  *)
-    (*   raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])) *)
-    (* else  *)
-      if not (type_in_type env) then
-      add_universe_constraints evd (Universes.Constraints.singleton (u1,Universes.ULe,u2))
-      else evd
+     if not (type_in_type env) then
+       add_universe_constraints evd (Universes.Constraints.singleton (u1,Universes.ULe,u2))
+     else evd
 	    
 let check_eq evd s s' =
   UGraph.check_eq (UState.ugraph evd.universes) s s'
@@ -901,10 +889,6 @@ let check_leq evd s s' =
 
 let normalize_evar_universe_context_variables = UState.normalize_variables
 
-(* let normvarsconstrkey = Profile.declare_profile "normalize_evar_universe_context_variables";; *)
-(* let normalize_evar_universe_context_variables = *)
-(*   Profile.profile1 normvarsconstrkey normalize_evar_universe_context_variables;; *)
-    
 let abstract_undefined_variables = UState.abstract_undefined_variables
 
 let fix_undefined_variables evd =
@@ -927,12 +911,6 @@ let nf_constraints evd =
   let uctx' = normalize_evar_universe_context uctx' in
     {evd with universes = uctx'}
 
-let nf_constraints = 
-  if Flags.profile then
-    let nfconstrkey = Profile.declare_profile "nf_constraints" in
-      Profile.profile1 nfconstrkey nf_constraints
-  else nf_constraints
-
 let universe_of_name evd s = UState.universe_of_name evd.universes s
 
 let add_universe_name evd s l =
diff --git a/engine/uState.ml b/engine/uState.ml
index c1aa75c09..75c03bc89 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -434,23 +434,21 @@ let refresh_undefined_univ_variables uctx =
     uctx', subst
 
 let normalize uctx = 
-  let rec fixpoint uctx = 
-    let ((vars',algs'), us') = 
-      Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables
-        uctx.uctx_univ_algebraic
+  let ((vars',algs'), us') = 
+    Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables
+				    uctx.uctx_univ_algebraic
+  in
+  if Univ.ContextSet.equal us' uctx.uctx_local then uctx
+  else
+    let us', universes =
+      Universes.refresh_constraints uctx.uctx_initial_universes us'
     in
-      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' = 
-          { uctx_names = uctx.uctx_names;
-            uctx_local = us'; 
-            uctx_univ_variables = vars'; 
-            uctx_univ_algebraic = algs';
-            uctx_universes = universes;
-            uctx_initial_universes = uctx.uctx_initial_universes }
-        in fixpoint uctx'
-  in fixpoint uctx
+      { uctx_names = uctx.uctx_names;
+        uctx_local = us'; 
+        uctx_univ_variables = vars'; 
+        uctx_univ_algebraic = algs';
+        uctx_universes = universes;
+        uctx_initial_universes = uctx.uctx_initial_universes }
 
 let universe_of_name uctx s = 
   UNameMap.find s (fst uctx.uctx_names)
diff --git a/engine/uState.mli b/engine/uState.mli
index 3a6f77e14..a188a5269 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -44,7 +44,7 @@ val ugraph : t -> UGraph.t
 
 val algebraics : t -> Univ.LSet.t
 (** The subset of unification variables that can be instantiated with algebraic
-    universes as they appear in types and universe instances only. *)
+    universes as they appear in inferred types only. *)
 
 val constraints : t -> Univ.constraints
 (** Shorthand for {!context_set} composed with {!ContextSet.constraints}. *)