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/standard/Tactics_standard.v | 65 ++++++++++++++++++++++++++++++++ 1 file changed, 65 insertions(+) create mode 100644 src/versions/standard/Tactics_standard.v (limited to 'src/versions/standard/Tactics_standard.v') 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: +*) -- cgit