aboutsummaryrefslogtreecommitdiffstats
path: root/src/versions/native/Tactics_native.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/versions/native/Tactics_native.v')
-rw-r--r--src/versions/native/Tactics_native.v55
1 files changed, 0 insertions, 55 deletions
diff --git a/src/versions/native/Tactics_native.v b/src/versions/native/Tactics_native.v
deleted file mode 100644
index 9b8d670..0000000
--- a/src/versions/native/Tactics_native.v
+++ /dev/null
@@ -1,55 +0,0 @@
-(**************************************************************************)
-(* *)
-(* SMTCoq *)
-(* Copyright (C) 2011 - 2022 *)
-(* *)
-(* 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:
-*)