From d5c3569d20253166487482dfb69716985943863c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 21 Jun 2016 08:43:30 +0200
Subject: Optimization in the subst tactic.

Do not evar-normalize the term to substitute with. The engine should be
insensitive to this kind of modification.
---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 3ba058e7f4..e264505314 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2928,7 +2928,7 @@ let unfold_body x =
   let xval = match Context.Named.lookup x hyps with
   | LocalAssum _ -> errorlabstrm "unfold_body"
     (pr_id x ++ str" is not a defined hypothesis.")
-  | LocalDef (_,xval,_) -> pf_nf_evar gl xval
+  | LocalDef (_,xval,_) -> xval
   in
   Tacticals.New.afterHyp x begin fun aft ->
   let hl = List.fold_right (fun decl cl -> (get_id decl, InHyp) :: cl) aft [] in
-- 
cgit v1.2.3