blob: d0ebb6162e70e664b8a3d3c293607af792733d8a (
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
56
57
58
59
60
61
62
63
|
(**************************************************************************)
(* *)
(* 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 *)
(* *)
(**************************************************************************)
val parse_certif :
CoqInterface.id ->
CoqInterface.id ->
CoqInterface.id ->
CoqInterface.id ->
CoqInterface.id ->
CoqInterface.id ->
CoqInterface.id ->
SmtBtype.reify_tbl * SmtAtom.Op.reify_tbl *
SmtAtom.Atom.reify_tbl * SmtAtom.Form.reify *
SmtAtom.Form.t list * int * SmtAtom.Form.t SmtCertif.clause ->
unit
val checker_debug :
SmtBtype.reify_tbl * SmtAtom.Op.reify_tbl *
SmtAtom.Atom.reify_tbl * SmtAtom.Form.reify *
SmtAtom.Form.t list * int * SmtAtom.Form.t SmtCertif.clause -> 'a
val theorem :
CoqInterface.id ->
SmtBtype.reify_tbl * SmtAtom.Op.reify_tbl *
SmtAtom.Atom.reify_tbl * SmtAtom.Form.reify *
SmtAtom.Form.t list * int * SmtAtom.Form.t SmtCertif.clause ->
unit
val checker :
SmtBtype.reify_tbl * SmtAtom.Op.reify_tbl *
SmtAtom.Atom.reify_tbl * SmtAtom.Form.reify *
SmtAtom.Form.t list * int * SmtAtom.Form.t SmtCertif.clause ->
unit
val tactic :
(Environ.env ->
SmtBtype.reify_tbl ->
SmtAtom.Op.reify_tbl ->
SmtAtom.Atom.reify_tbl ->
SmtAtom.Form.reify ->
(SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t) ->
SmtAtom.Form.t list -> int * SmtAtom.Form.t SmtCertif.clause) ->
SmtMisc.logic ->
SmtBtype.reify_tbl ->
SmtAtom.Op.reify_tbl ->
SmtAtom.Atom.reify_tbl ->
SmtAtom.Form.reify ->
SmtAtom.Atom.reify_tbl ->
SmtAtom.Form.reify ->
(Environ.env -> CoqInterface.constr -> CoqInterface.constr) ->
CoqInterface.constr list ->
CoqInterface.constr_expr list -> CoqInterface.tactic
val model_string : Environ.env -> SmtBtype.reify_tbl -> 'a -> 'b -> 'c -> SExpr.t -> string
|
