Merge branch 'trunk' into located_switch

1 files changed, 10 insertions, 6 deletions

diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index b4a0e46ae..5adf8475a 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -18,7 +18,7 @@ open Glob_term
 open Geninterp
 open Extraargs
 open Tacmach
-open Tacticals
+open Proofview.Notations
 open Rewrite
 open Stdarg
 open Pcoq.Vernac_
@@ -123,15 +123,19 @@ TACTIC EXTEND rewrite_strat
 END
 
 let clsubstitute o c =
-  let is_tac id = match fst (fst (snd c)) with { CAst.v = GVar id'} when Id.equal id' id -> true | _ -> false in
-    Tacticals.onAllHypsAndConcl
+  Proofview.Goal.enter { enter = begin fun gl ->
+  let is_tac id = match fst (fst (snd c)) with { CAst.v = GVar id' } when Id.equal id' id -> true | _ -> false in
+  let hyps = Tacmach.New.pf_ids_of_hyps gl in
+    Tacticals.New.tclMAP
       (fun cl ->
         match cl with
-          | Some id when is_tac id -> tclIDTAC
-          | _ -> Proofview.V82.of_tactic (cl_rewrite_clause c o AllOccurrences cl))
+          | Some id when is_tac id -> Tacticals.New.tclIDTAC
+          | _ -> cl_rewrite_clause c o AllOccurrences cl)
+      (None :: List.map (fun id -> Some id) hyps)
+  end }
 
 TACTIC EXTEND substitute
-| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ Proofview.V82.tactic (clsubstitute o c) ]
+| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ clsubstitute o c ]
 END