diff options
Diffstat (limited to 'plugins/ltac/g_rewrite.ml4')
-rw-r--r-- | plugins/ltac/g_rewrite.ml4 | 16 |
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 |