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.

1 files changed, 11 insertions, 7 deletions

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