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.

6 files changed, 37 insertions, 23 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index 298302815..04f55f2c3 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -609,7 +609,10 @@ let vars_of_global_reference env gr =
    [m] is appropriately lifted through abstractions of [t] *)
 
 let dependent_main noevar univs m t =
-  let eqc x y = if univs then fst (Universes.eq_constr_universes x y) else eq_constr_nounivs x y in
+  let eqc x y =
+    if univs then not (Option.is_empty (Universes.eq_constr_universes x y))
+    else eq_constr_nounivs x y
+  in
   let rec deprec m t =
     if eqc m t then
       raise Occur
diff --git a/engine/universes.ml b/engine/universes.ml
index 0573dd2c6..6720fcef8 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -199,7 +199,7 @@ let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu =
   if res then Some !cstrs else None
 
 let test_constr_universes leq m n =
-  if m == n then true, Constraints.empty
+  if m == n then Some Constraints.empty
   else 
     let cstrs = ref Constraints.empty in
     let eq_universes strict l l' = 
@@ -229,7 +229,7 @@ let test_constr_universes leq m n =
       else
         Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
     in
-    res, !cstrs
+    if res then Some !cstrs else None
 
 let eq_constr_universes m n = test_constr_universes false m n
 let leq_constr_universes m n = test_constr_universes true m n
diff --git a/engine/universes.mli b/engine/universes.mli
index 0aeea91cd..725c21d29 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -88,11 +88,11 @@ val leq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator ->
 
 (** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts,
     application grouping and the universe constraints in [c]. *)
-val eq_constr_universes : constr -> constr -> bool universe_constrained
+val eq_constr_universes : constr -> constr -> universe_constraints option
 
 (** [leq_constr_universes a b] [true, c] if [a] is convertible to [b] modulo
     alpha, casts, application grouping and the universe constraints in [c]. *)
-val leq_constr_universes : constr -> constr -> bool universe_constrained
+val leq_constr_universes : constr -> constr -> universe_constraints option
 
 (** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts,
     application grouping and the universe constraints in [c]. *)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3ef0bb1b3..d06009dce 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 0ab941b34..a85e493ea 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 e73c5ffaf..e2b3af7e9 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