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/native/Tactics_native.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/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: +*) |