From a09f5ba40039c0f367c320986011c2d08b953c5b Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Wed, 6 Nov 2013 14:52:19 +0000
Subject: Less partial applications in Vars, as well as better memory
 allocation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17065 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/goal.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/goal.ml b/proofs/goal.ml
index ebd6ca84db..a036f728d5 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -433,9 +433,12 @@ let convert_concl check cl' = (); fun env rdefs gl info ->
 
 (* Renames a hypothesis. *)
 let rename_hyp_sign id1 id2 sign =
+  let subst = [id1,mkVar id2] in
+  let replace_vars c = replace_vars subst c in
   Environ.apply_to_hyp_and_dependent_on sign id1
     (fun (_,b,t) _ -> (id2,b,t))
-    (fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d)
+    (fun d _ -> map_named_declaration replace_vars d)
+
 let rename_hyp id1 id2 = (); fun env rdefs gl info ->
   let hyps = hyps env rdefs gl info in
   if not (Names.Id.equal id1 id2) &&
-- 
cgit v1.2.3