From 103ec7205d9038f1f3821f9287e3bb0907a1e3ec Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 19 Nov 2015 13:36:31 +0100
Subject: More efficient implementation of equality-up-to-universes in
 Universes.

Instead of accumulating constraints which are not present in the original
graph, we parametrize the equality function by a function actually merging
those constraints in the current graph. This prevents doing the work twice.
---
 engine/evd.ml | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

(limited to 'engine')

diff --git a/engine/evd.ml b/engine/evd.ml
index 069fcbfa6e..00a869fda8 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -962,11 +962,13 @@ let test_conversion env d pb t u =
 exception UniversesDiffer = UState.UniversesDiffer
 
 let eq_constr_univs evd t u =
-  let b, c = Universes.eq_constr_univs_infer (UState.ugraph evd.universes) t u in
-    if b then 
-      try let evd' = add_universe_constraints evd c in evd', b
-      with Univ.UniverseInconsistency _ | UniversesDiffer -> evd, false
-    else evd, b
+  let fold cstr sigma =
+    try Some (add_universe_constraints sigma cstr)
+    with Univ.UniverseInconsistency _ | UniversesDiffer -> None
+  in
+  match Universes.eq_constr_univs_infer (UState.ugraph evd.universes) fold t u evd with
+  | None -> evd, false
+  | Some evd -> evd, true
 
 let e_eq_constr_univs evdref t u =
   let evd, b = eq_constr_univs !evdref t u in
-- 
cgit v1.2.3