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.
---
 tactics/tactics.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0a013e95f7..0551787e3a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1319,7 +1319,9 @@ let simplest_elim c = default_elim false None (c,NoBindings)
 *)
 
 let clenv_fchain_in id ?(flags=elim_flags ()) mv elimclause hypclause =
-  try clenv_fchain ~flags mv elimclause hypclause
+  (** The evarmap of elimclause is assumed to be an extension of hypclause, so
+      we do not need to merge the universes coming from hypclause. *)
+  try clenv_fchain ~with_univs:false ~flags mv elimclause hypclause
   with PretypeError (env,evd,NoOccurrenceFound (op,_)) ->
     (* Set the hypothesis name in the message *)
     raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id)))
-- 
cgit v1.2.3