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 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'engine/termops.ml')

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