diff options
| author | QGarchery <QGarchery@users.noreply.github.com> | 2019-02-08 07:51:05 +0100 |
|---|---|---|
| committer | ckeller <ckeller@users.noreply.github.com> | 2019-02-08 07:51:05 +0100 |
| commit | 05fc195f4e6e0a194323e68efa0d18dafece96ae (patch) | |
| tree | d8e1ec8805a5334c6e0967c599ad437513bcae6d /src | |
| parent | d813320d18db7c065cb8fda0cdc5785045d1a6c8 (diff) | |
| download | smtcoq-05fc195f4e6e0a194323e68efa0d18dafece96ae.tar.gz smtcoq-05fc195f4e6e0a194323e68efa0d18dafece96ae.zip | |
tactic notations (#31)
Diffstat (limited to 'src')
| -rw-r--r-- | src/Tactics.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/Tactics.v b/src/Tactics.v index 23818fb..4e193ca 100644 --- a/src/Tactics.v +++ b/src/Tactics.v @@ -74,11 +74,11 @@ Ltac vauto := apply H); auto. -Ltac verit_bool := - verit_bool_base; vauto. +Tactic Notation "verit_bool" constr_list(h) := + verit_bool_base h; vauto. -Ltac verit_bool_no_check := - verit_bool_no_check_base; vauto. +Tactic Notation "verit_bool_no_check" constr_list(h) := + verit_bool_no_check_base h; vauto. (** Tactics in Prop **) @@ -86,8 +86,8 @@ Ltac verit_bool_no_check := Ltac zchaff := prop2bool; zchaff_bool; bool2prop. Ltac zchaff_no_check := prop2bool; zchaff_bool_no_check; bool2prop. -Ltac verit := prop2bool; verit_bool; bool2prop. -Ltac verit_no_check := prop2bool; verit_bool_no_check; bool2prop. +Tactic Notation "verit" constr_list(h) := prop2bool; verit_bool h; bool2prop. +Tactic Notation "verit_no_check" constr_list(h) := prop2bool; verit_bool_no_check h; bool2prop. Ltac cvc4 := prop2bool; cvc4_bool; bool2prop. Ltac cvc4_no_check := prop2bool; cvc4_bool_no_check; bool2prop. @@ -110,5 +110,5 @@ Ltac cvc4_no_check := prop2bool; cvc4_bool_no_check; bool2prop. (* end; *) (* bool2prop. *) -Ltac smt := (prop2bool; try verit_bool; cvc4_bool; try verit_bool; bool2prop). +Tactic Notation "smt" constr_list(h) := (prop2bool; try verit_bool h; cvc4_bool; try verit_bool h; bool2prop). Ltac smt_no_check := (prop2bool; try verit_bool_no_check; cvc4_bool_no_check; try verit_bool_no_check; bool2prop). |