From 02544aa0e9f2693de4b02a87d8e66cc8e72e3c8b Mon Sep 17 00:00:00 2001 From: ckeller Date: Fri, 12 Apr 2019 14:13:00 +0200 Subject: Error message to state that tactics are not supported with native-coq (#47) * Better error message for failing tactics with native-coq --- src/versions/native/Tactics_native.v | 55 ++++++++++++++++++++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 src/versions/native/Tactics_native.v (limited to 'src/versions/native/Tactics_native.v') 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: +*) -- cgit