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.

1 files changed, 10 insertions, 6 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 52f424f75..dcb19b31a 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