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.

1 files changed, 4 insertions, 6 deletions

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index bd2074139..fbcd9ee2d 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