diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2019-09-20 11:07:47 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2019-09-20 11:07:47 +0200 |
| commit | a17e48674bace4df1509b0624bef85128d81afbf (patch) | |
| tree | 97e2ae715bfbe4fcf40d3e9706954055d0a0f39b /src/Tactics.v | |
| parent | 9b80b60bbf8bc7ec0ce8985b66399a179126882d (diff) | |
| download | smtcoq-a17e48674bace4df1509b0624bef85128d81afbf.tar.gz smtcoq-a17e48674bace4df1509b0624bef85128d81afbf.zip | |
Remove unused file
Diffstat (limited to 'src/Tactics.v')
| -rw-r--r-- | src/Tactics.v | 65 |
1 files changed, 0 insertions, 65 deletions
diff --git a/src/Tactics.v b/src/Tactics.v deleted file mode 100644 index 95b92d6..0000000 --- a/src/Tactics.v +++ /dev/null @@ -1,65 +0,0 @@ -(**************************************************************************) -(* *) -(* 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: -*) |