From 1eea5f0081264ccb01a12f682734e8a624f83804 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 20 Jun 2016 19:54:13 +0200
Subject: Optimization in the subst tactic.

We use simple variable substitution instead of full-power term
matching.
---
 tactics/tactics.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c336bb434a..3ba058e7f4 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2932,8 +2932,7 @@ let unfold_body x =
   in
   Tacticals.New.afterHyp x begin fun aft ->
   let hl = List.fold_right (fun decl cl -> (get_id decl, InHyp) :: cl) aft [] in
-  let xvar = mkVar x in
-  let rfun _ _ c = replace_term xvar xval c in
+  let rfun _ _ c = replace_vars [x, xval] c in
   let reducth h = reduct_in_hyp rfun h in
   let reductc = reduct_in_concl (rfun, DEFAULTcast) in
   Tacticals.New.tclTHENLIST [Tacticals.New.tclMAP reducth hl; reductc]
-- 
cgit v1.2.3