diff options
Diffstat (limited to 'src/tac2stdlib.ml')
| -rw-r--r-- | src/tac2stdlib.ml | 6 |
1 files changed, 6 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 |