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.
---
 engine/termops.ml    | 5 ++++-
 engine/universes.ml  | 4 ++--
 engine/universes.mli | 4 ++--
 3 files changed, 8 insertions(+), 5 deletions(-)

(limited to 'engine')

diff --git a/engine/termops.ml b/engine/termops.ml
index 298302815a..04f55f2c35 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 0573dd2c60..6720fcef8f 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 0aeea91cdc..725c21d296 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]. *)
-- 
cgit v1.2.3