aboutsummaryrefslogtreecommitdiffstats
path: root/src/verit/verit.mli
diff options
context:
space:
mode:
authorckeller <ckeller@users.noreply.github.com>2019-03-11 20:25:35 +0100
committerGitHub <noreply@github.com>2019-03-11 20:25:35 +0100
commita88e3b3b6ad01a9b85c828b9a1225732275affee (patch)
treeacc3768695698a80867b4ce941ab4cb7b4b99d7a /src/verit/verit.mli
parent33010bfa6345549d8b9b0c06f44150b60d0c86e5 (diff)
downloadsmtcoq-a88e3b3b6ad01a9b85c828b9a1225732275affee.tar.gz
smtcoq-a88e3b3b6ad01a9b85c828b9a1225732275affee.zip
V8.8 (#42)
* Towards 8.8 * Towards 8.8 * Towards 8.8 * Towards 8.8 * Towards 8.8 * Towards 8.8 * Towards 8.8 * Organization structures * 8.8 ok with standard coq
Diffstat (limited to 'src/verit/verit.mli')
-rw-r--r--src/verit/verit.mli16
1 files changed, 8 insertions, 8 deletions
diff --git a/src/verit/verit.mli b/src/verit/verit.mli
index 468aa1e..6fa62d8 100644
--- a/src/verit/verit.mli
+++ b/src/verit/verit.mli
@@ -11,13 +11,13 @@
val parse_certif :
- Structures.names_id ->
- Structures.names_id ->
- Structures.names_id ->
- Structures.names_id ->
- Structures.names_id -> Structures.names_id -> Structures.names_id -> string -> string -> unit
+ Structures.id ->
+ Structures.id ->
+ Structures.id ->
+ Structures.id ->
+ Structures.id -> Structures.id -> Structures.id -> string -> string -> unit
val checker : string -> string -> unit
val checker_debug : string -> string -> unit
-val theorem : Structures.names_id -> string -> string -> unit
-val tactic : Term.constr list -> Structures.constr_expr list -> Structures.tactic
-val tactic_no_check : Term.constr list -> Structures.constr_expr list -> Structures.tactic
+val theorem : Structures.id -> string -> string -> unit
+val tactic : Structures.constr list -> Structures.constr_expr list -> Structures.tactic
+val tactic_no_check : Structures.constr list -> Structures.constr_expr list -> Structures.tactic