From bd170eb3937aa55f665a671fe9d2916a26af2a09 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 21 Jun 2016 17:09:25 +0200
Subject: Optimize the subst tactic.

Do not evar-normalize the argument provided by afterHyp.
---
 tactics/tacticals.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 3d51623eaa..46145d1116 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -590,8 +590,8 @@ module New = struct
   let onHyps find tac = Proofview.Goal.nf_enter { enter = begin fun gl -> tac (find.enter gl) end }
 
   let afterHyp id tac =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
-    let hyps = Proofview.Goal.hyps gl in
+    Proofview.Goal.enter { enter = begin fun gl ->
+    let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
     let rem, _ = List.split_when (Id.equal id % get_id) hyps in
     tac rem
     end }
-- 
cgit v1.2.3