From e12110637730d067c216abcc86185b761189b342 Mon Sep 17 00:00:00 2001
From: vblot <24938579+vblot@users.noreply.github.com>
Date: Fri, 28 May 2021 18:29:37 +0200
Subject: getting rid of native-coq (#95)

---
 src/versions/native/Tactics_native.v | 55 ------------------------------------
 1 file changed, 55 deletions(-)
 delete 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
deleted file mode 100644
index 45d3603..0000000
--- a/src/versions/native/Tactics_native.v
+++ /dev/null
@@ -1,55 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     SMTCoq                                                             *)
-(*     Copyright (C) 2011 - 2021                                          *)
-(*                                                                        *)
-(*     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