diff options
author | ckeller <ckeller@users.noreply.github.com> | 2019-04-12 14:13:00 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-04-12 14:13:00 +0200 |
commit | 02544aa0e9f2693de4b02a87d8e66cc8e72e3c8b (patch) | |
tree | ec18dc8768ea8ca45ed380ffda289fe204a822a5 /src/versions/standard/Tactics_standard.v | |
parent | ad491f845f6fb3e88ff1169ac472f194d12306d2 (diff) | |
download | smtcoq-02544aa0e9f2693de4b02a87d8e66cc8e72e3c8b.tar.gz smtcoq-02544aa0e9f2693de4b02a87d8e66cc8e72e3c8b.zip |
Error message to state that tactics are not supported with native-coq (#47)
* Better error message for failing tactics with native-coq
Diffstat (limited to 'src/versions/standard/Tactics_standard.v')
-rw-r--r-- | src/versions/standard/Tactics_standard.v | 65 |
1 files changed, 65 insertions, 0 deletions
diff --git a/src/versions/standard/Tactics_standard.v b/src/versions/standard/Tactics_standard.v new file mode 100644 index 0000000..95b92d6 --- /dev/null +++ b/src/versions/standard/Tactics_standard.v @@ -0,0 +1,65 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2019 *) +(* *) +(* See file "AUTHORS" for the list of authors *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + + +Require Import PropToBool BoolToProp. (* Before SMTCoq.State *) +Require Import Int63 List PArray Bool ZArith. +Require Import SMTCoq.State SMTCoq.SMT_terms SMTCoq.Trace SMT_classes_instances QInst. + +Declare ML Module "smtcoq_plugin". + + +Tactic Notation "verit_bool" constr_list(h) := + verit_bool_base h; vauto. + +Tactic Notation "verit_bool_no_check" constr_list(h) := + verit_bool_no_check_base h; vauto. + + +(** Tactics in Prop **) + +Ltac zchaff := prop2bool; zchaff_bool; bool2prop. +Ltac zchaff_no_check := prop2bool; zchaff_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. + + +(* Ltac smt := prop2bool; *) +(* repeat *) +(* match goal with *) +(* | [ |- context[ CompDec ?t ] ] => try assumption *) +(* | [ |- _ : bool] => verit_bool *) +(* | [ |- _ : bool] => try (cvc4_bool; verit_bool) *) +(* end; *) +(* bool2prop. *) +(* Ltac smt_no_check := prop2bool; *) +(* repeat *) +(* match goal with *) +(* | [ |- context[ CompDec ?t ] ] => try assumption *) +(* | [ |- _ : bool] => verit_bool_no_check *) +(* | [ |- _ : bool] => try (cvc4_bool_no_check; verit_bool_no_check) *) +(* end; *) +(* bool2prop. *) + +Tactic Notation "smt" constr_list(h) := (prop2bool; try verit_bool h; cvc4_bool; try verit_bool h; bool2prop). +Tactic Notation "smt_no_check" constr_list(h) := (prop2bool; try verit_bool_no_check h; cvc4_bool_no_check; try verit_bool_no_check h; bool2prop). + + + +(* + Local Variables: + coq-load-path: ((rec "." "SMTCoq")) + End: +*) |