diff options
Diffstat (limited to 'src/versions/native/Tactics_native.v')
| -rw-r--r-- | src/versions/native/Tactics_native.v | 55 |
1 files changed, 55 insertions, 0 deletions
diff --git a/src/versions/native/Tactics_native.v b/src/versions/native/Tactics_native.v new file mode 100644 index 0000000..d2b2400 --- /dev/null +++ b/src/versions/native/Tactics_native.v @@ -0,0 +1,55 @@ +(**************************************************************************) +(* *) +(* 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 Psatz. + +Declare ML Module "smtcoq_plugin". + + + +Tactic Notation "verit_bool" constr_list(h) := + fail "Tactics are not supported with native-coq". + +Tactic Notation "verit_bool_no_check" constr_list(h) := + fail "Tactics are not supported with native-coq". + + +(** Tactics in Prop **) + +Ltac zchaff := + fail "Tactics are not supported with native-coq". +Ltac zchaff_no_check := + fail "Tactics are not supported with native-coq". + +Tactic Notation "verit" constr_list(h) := + fail "Tactics are not supported with native-coq". +Tactic Notation "verit_no_check" constr_list(h) := + fail "Tactics are not supported with native-coq". + +Ltac cvc4 := + fail "Tactics are not supported with native-coq". +Ltac cvc4_no_check := + fail "Tactics are not supported with native-coq". + + +Tactic Notation "smt" constr_list(h) := + fail "Tactics are not supported with native-coq". +Tactic Notation "smt_no_check" constr_list(h) := + fail "Tactics are not supported with native-coq". + + + +(* + Local Variables: + coq-load-path: ((rec "../.." "SMTCoq")) + End: +*) |