Stronger static invariant in equality upto universes.

We return an option type, as constraints were always dropped if the boolean
was false. They did not make much sense anyway.

3 files changed, 29 insertions, 18 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3ef0bb1b35..d06009dce5 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -401,14 +401,16 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     else evar_eqappr_x ts env' evd CONV out2 out1
   in
   let rigids env evd sk term sk' term' =
-    let b,univs = Universes.eq_constr_universes term term' in
-      if b then
+    let univs = Universes.eq_constr_universes term term' in
+    match univs with
+    | Some univs ->
        ise_and evd [(fun i ->
          let cstrs = Universes.to_constraints (Evd.universes i) univs in
            try Success (Evd.add_constraints i cstrs)
            with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
                   (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')]
-      else UnifFailure (evd,NotSameHead)
+    | None ->
+      UnifFailure (evd,NotSameHead)
   in
   let flex_maybeflex on_left ev ((termF,skF as apprF),cstsF) ((termM, skM as apprM),cstsM) vM =
     let switch f a b = if on_left then f a b else f b a in
@@ -650,14 +652,16 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	     allow this identification (first-order unification of universes). Otherwise
 	     fallback to unfolding.
 	  *)
-	  let b,univs = Universes.eq_constr_universes term1 term2 in
-	    if b then
+	  let univs = Universes.eq_constr_universes term1 term2 in
+          match univs with
+          | Some univs ->
 	      ise_and i [(fun i -> 
 		try Success (Evd.add_universe_constraints i univs)
 		with UniversesDiffer -> UnifFailure (i,NotSameHead)
 		| Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
 			 (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
-	    else UnifFailure (i,NotSameHead)
+          | None ->
+            UnifFailure (i,NotSameHead)
 	and f2 i =
 	  (try 
 	     if not (snd ts) then raise Not_found
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 0ab941b346..a85e493eae 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -681,13 +681,17 @@ let magicaly_constant_of_fixbody env reference bd = function
       match constant_opt_value_in env (cst,u) with
       | None -> bd
       | Some t ->
-        let b, csts = Universes.eq_constr_universes t bd in
-    	let subst = Universes.Constraints.fold (fun (l,d,r) acc ->
-    	  Univ.LMap.add (Option.get (Universe.level l)) (Option.get (Universe.level r)) acc)
-    	  csts Univ.LMap.empty
-    	in
-    	let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in
-          if b then mkConstU (cst,inst) else bd
+        let csts = Universes.eq_constr_universes t bd in
+        begin match csts with
+        | Some csts ->
+          let subst = Universes.Constraints.fold (fun (l,d,r) acc ->
+            Univ.LMap.add (Option.get (Universe.level l)) (Option.get (Universe.level r)) acc)
+            csts Univ.LMap.empty
+          in
+          let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in
+          mkConstU (cst,inst)
+        | None -> bd
+        end
     with
     | Not_found -> bd
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e73c5ffaf3..e2b3af7e97 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -558,19 +558,22 @@ let force_eqs c =
     c Universes.Constraints.empty
 
 let constr_cmp pb sigma flags t u =
-  let b, cstrs = 
+  let cstrs =
     if pb == Reduction.CONV then Universes.eq_constr_universes t u
     else Universes.leq_constr_universes t u
   in 
-    if b then 
-      try Evd.add_universe_constraints sigma cstrs, b
+  match cstrs with
+  | Some cstrs ->
+      begin try Evd.add_universe_constraints sigma cstrs, true
       with Univ.UniverseInconsistency _ -> sigma, false
       | Evd.UniversesDiffer -> 
 	if is_rigid_head flags t then 
-	  try Evd.add_universe_constraints sigma (force_eqs cstrs), b
+	  try Evd.add_universe_constraints sigma (force_eqs cstrs), true
 	  with Univ.UniverseInconsistency _ -> sigma, false
 	else sigma, false
-    else sigma, b
+      end
+  | None ->
+    sigma, false
     
 let do_reduce ts (env, nb) sigma c =
   Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state