From c48838c05eea1793c2d0a11292f8fc4eb784cd02 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 31 Oct 2016 18:31:35 +0100
Subject: 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.
---
 pretyping/reductionops.ml | 18 +++++++++++-------
 1 file changed, 11 insertions(+), 7 deletions(-)

(limited to 'pretyping/reductionops.ml')

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
 
-- 
cgit v1.2.3