diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-16 22:58:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-16 23:00:13 +0200 |
| commit | ed1c4d01388bf11710b38f1c302d405233c24647 (patch) | |
| tree | 0ffc730e786e65e03d253ac6d8d4e506c45bd751 /tactics | |
| parent | fd5898afa9a89ca61f87cdeca4ae982a024e4d4b (diff) | |
Put the "change" tactic in the monad.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 10 | ||||
| -rw-r--r-- | tactics/tactics.mli | 2 |
2 files changed, 7 insertions, 5 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 59e6a1c82..83b8aacfe 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -825,14 +825,16 @@ let change_option occl t = function | Some id -> change_in_hyp occl t id | None -> change_in_concl occl t -let change chg c cls gl = - let cls = concrete_clause_of (fun () -> Tacmach.pf_ids_of_hyps gl) cls in - Proofview.V82.of_tactic (Tacticals.New.tclMAP (function +let change chg c cls = + Proofview.Goal.enter { enter = begin fun gl -> + let cls = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cls in + Tacticals.New.tclMAP (function | OnHyp (id,occs,where) -> change_option (bind_change_occurrences occs chg) c (Some (id,where)) | OnConcl occs -> change_option (bind_change_occurrences occs chg) c None) - cls) gl + cls + end } let change_concl t = change_in_concl None (make_change_arg t) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 6987e5b70..046a15d14 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -154,7 +154,7 @@ val unfold_in_hyp : val unfold_option : (occurrences * evaluable_global_reference) list -> goal_location -> unit Proofview.tactic val change : - constr_pattern option -> change_arg -> clause -> tactic + constr_pattern option -> change_arg -> clause -> unit Proofview.tactic val pattern_option : (occurrences * constr) list -> goal_location -> unit Proofview.tactic val reduce : red_expr -> clause -> unit Proofview.tactic |