From 866d2b75a2d213443e8498b4585326a955ed1558 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 30 Sep 2014 12:07:02 +0200
Subject: Semantic fix of a refine in Rewrite.

This code was wrong but luckily unused. It instantiated an evar with an
instance where the let-in bindings were removed.
---
 tactics/rewrite.ml | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index bd20741399..fbcd9ee2da 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1519,13 +1519,11 @@ let assert_replacing id newt tac =
       let env' = Environ.reset_with_named_context (val_of_named_context nc') env in
       let h, ev = Proofview.Refine.new_evar h env' concl in
       let h, ev' = Proofview.Refine.new_evar h env newt in
-      let inst =
-        fold_named_context
-          (fun _ (n, b, t) inst ->
-              if Id.equal n id then ev' :: inst
-              else if Option.is_empty b then mkVar n :: inst else inst)
-          env ~init:[]
+      let fold _ (n, b, t) inst =
+        if Id.equal n id then ev' :: inst
+        else mkVar n :: inst
       in
+      let inst = fold_named_context fold env ~init:[] in
       let (e, args) = destEvar ev in
       h, mkEvar (e, Array.of_list inst)
     end
-- 
cgit v1.2.3