blob: 45d36037c66c59485c2c173d3d9813c39ced9ee4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
|
(**************************************************************************)
(* *)
(* 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:
*)
|
