From af399d81b0505d1f0be8e73cf45044266d5749e5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 17 Nov 2015 12:39:35 +0100
Subject: Performance fix for destruct.

The clenv_fchain function was needlessly merging universes coming from
two evarmaps even though one was an extension of the other. A flag was
added so that the tactic just retrieves the newer universes.
---
 proofs/clenv.ml  | 4 ++--
 proofs/clenv.mli | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index a2cccc0e0b..5de8338ab6 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -379,12 +379,12 @@ let fchain_flags () =
   { (default_unify_flags ()) with
     allow_K_in_toplevel_higher_order_unification = true }
 
-let clenv_fchain ?(flags=fchain_flags ()) mv clenv nextclenv =
+let clenv_fchain ?with_univs ?(flags=fchain_flags ()) mv clenv nextclenv =
   (* Add the metavars of [nextclenv] to [clenv], with their name-environment *)
   let clenv' =
     { templval = clenv.templval;
       templtyp = clenv.templtyp;
-      evd = meta_merge nextclenv.evd clenv.evd;
+      evd = meta_merge ?with_univs nextclenv.evd clenv.evd;
       env = nextclenv.env } in
   (* unify the type of the template of [nextclenv] with the type of [mv] *)
   let clenv'' =
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index eb10817069..26e803354e 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -51,7 +51,7 @@ val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst
 
 val connect_clenv : Goal.goal sigma -> clausenv -> clausenv
 val clenv_fchain :
-  ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv
+  ?with_univs:bool -> ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv
 
 (** {6 Unification with clenvs } *)
 
-- 
cgit v1.2.3