aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace/smtCommands.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/trace/smtCommands.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/trace/smtCommands.mli')
-rw-r--r--src/trace/smtCommands.mli20
1 files changed, 10 insertions, 10 deletions
diff --git a/src/trace/smtCommands.mli b/src/trace/smtCommands.mli
index d7b6ae6..9a1b681 100644
--- a/src/trace/smtCommands.mli
+++ b/src/trace/smtCommands.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 ->
+ Structures.id ->
+ Structures.id ->
+ Structures.id ->
+ Structures.id ->
+ Structures.id ->
+ Structures.id ->
+ Structures.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 ->
@@ -29,7 +29,7 @@ val checker_debug :
SmtAtom.Form.t list * int * SmtAtom.Form.t SmtCertif.clause -> 'a
val theorem :
- Structures.names_id ->
+ Structures.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 ->
@@ -56,8 +56,8 @@ val tactic :
SmtAtom.Form.reify ->
SmtAtom.Atom.reify_tbl ->
SmtAtom.Form.reify ->
- (Environ.env -> Term.constr -> Term.constr) ->
- Term.constr list ->
+ (Environ.env -> Structures.constr -> Structures.constr) ->
+ Structures.constr list ->
Structures.constr_expr list -> Structures.tactic
val model_string : Environ.env -> SmtBtype.reify_tbl -> 'a -> 'b -> 'c -> SExpr.t -> string