diff options
| author | Maxime Dénès | 2017-06-06 17:18:59 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-06 17:18:59 +0200 |
| commit | e5581b2a1e5b3d9fc5dc7fe95ee4ba121f5d42cd (patch) | |
| tree | 1a0d0b7d693c37ca8712057e946587584687208e /plugins/ltac/g_rewrite.ml4 | |
| parent | 2f23c27e08f66402b8fba4745681becd402f4c5c (diff) | |
| parent | 0ce9cef0ac431e184c870617841bedc3f427396d (diff) | |
Merge PR#623: Remove the Sigma (monotonous state) API.
Diffstat (limited to 'plugins/ltac/g_rewrite.ml4')
| -rw-r--r-- | plugins/ltac/g_rewrite.ml4 | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index 5adf8475ae..25258ffa90 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -18,7 +18,6 @@ open Glob_term open Geninterp open Extraargs open Tacmach -open Proofview.Notations open Rewrite open Stdarg open Pcoq.Vernac_ @@ -123,7 +122,7 @@ TACTIC EXTEND rewrite_strat END let clsubstitute o c = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.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 @@ -132,7 +131,7 @@ let clsubstitute o c = | 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 } + end TACTIC EXTEND substitute | [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ clsubstitute o c ] |