From e22796a610853d8e7ff64785c98004d8ceac98e3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 12 May 2017 15:16:24 +0200
Subject: Postponing of universe constraints unification in term equality.

Instead of calling the universe unification at each term node, we accumulate
them and try to perform unification at the very end. This seems to be
experimentally faster.
---
 pretyping/reductionops.ml | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 52f424f751..dcb19b31af 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1317,19 +1317,23 @@ let sigma_univ_state =
 let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
     ?(ts=full_transparent_state) env sigma x y =
   (** FIXME *)
+  let open Universes in
   let x = EConstr.Unsafe.to_constr x in
   let y = EConstr.Unsafe.to_constr y in
   try
-    let fold cstr sigma =
-      try Some (Evd.add_universe_constraints sigma cstr)
-      with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> None
-    in
+    let fold cstr accu = Some (Constraints.fold Constraints.add cstr accu) in
     let b, sigma = 
       let ans =
 	if pb == Reduction.CUMUL then 
-	  Universes.leq_constr_univs_infer (Evd.universes sigma) fold x y sigma
+	  Universes.leq_constr_univs_infer (Evd.universes sigma) fold x y Constraints.empty
 	else
-	  Universes.eq_constr_univs_infer (Evd.universes sigma) fold x y sigma
+	  Universes.eq_constr_univs_infer (Evd.universes sigma) fold x y Constraints.empty
+      in
+      let ans = match ans with
+      | None -> None
+      | Some cstr ->
+        try Some (Evd.add_universe_constraints sigma cstr)
+        with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> None
       in
       match ans with
       | None -> false, sigma
-- 
cgit v1.2.3