diff options
| author | Pierre-Marie Pédrot | 2017-11-02 11:41:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-11-02 11:52:17 +0100 |
| commit | 62606e17ff4afe6a897607d45471b7f4d3ef54b8 (patch) | |
| tree | 972102473076ef38585c909444a266f780b95a80 /src | |
| parent | de7483beb78e5bd81dc6449ba201fb9dfc490ba8 (diff) | |
Binding the specialize tactic.
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2stdlib.ml | 6 | ||||
| -rw-r--r-- | src/tac2tactics.ml | 5 | ||||
| -rw-r--r-- | src/tac2tactics.mli | 2 |
3 files changed, 13 insertions, 0 deletions
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml index 60b6e70d58..6026b5b319 100644 --- a/src/tac2stdlib.ml +++ b/src/tac2stdlib.ml @@ -569,6 +569,12 @@ let () = define_prim3 "tac_constructorn" begin fun ev n bnd -> Tac2tactics.constructor_tac ev None n bnd end +let () = define_prim2 "tac_specialize" begin fun c ipat -> + let c = to_constr_with_bindings c in + let ipat = Value.to_option to_intro_pattern ipat in + Tac2tactics.specialize c ipat +end + let () = define_prim1 "tac_symmetry" begin fun cl -> let cl = to_clause cl in Tac2tactics.symmetry cl diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml index f7ad057e86..eec0d2ab45 100644 --- a/src/tac2tactics.ml +++ b/src/tac2tactics.ml @@ -150,6 +150,11 @@ let split_with_bindings ev bnd = let bnd = mk_bindings bnd in Tactics.split_with_bindings ev [bnd] +let specialize c pat = + let c = mk_with_bindings c in + let pat = Option.map mk_intro_pattern pat in + Tactics.specialize c pat + let change pat c cl = let open Tac2ffi in Proofview.Goal.enter begin fun gl -> diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli index 7a4624ba2c..96c7b9214c 100644 --- a/src/tac2tactics.mli +++ b/src/tac2tactics.mli @@ -38,6 +38,8 @@ val left_with_bindings : evars_flag -> bindings -> unit tactic val right_with_bindings : evars_flag -> bindings -> unit tactic val split_with_bindings : evars_flag -> bindings -> unit tactic +val specialize : constr_with_bindings -> intro_pattern option -> unit tactic + val change : Pattern.constr_pattern option -> (constr array, constr) Tac2ffi.fun1 -> clause -> unit tactic val rewrite : |