aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace/smtCommands.mli
diff options
context:
space:
mode:
Diffstat (limited to 'src/trace/smtCommands.mli')
-rw-r--r--src/trace/smtCommands.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/trace/smtCommands.mli b/src/trace/smtCommands.mli
index b90e3ff..d6fa756 100644
--- a/src/trace/smtCommands.mli
+++ b/src/trace/smtCommands.mli
@@ -80,7 +80,7 @@ val core_tactic :
SmtAtom.Op.reify_tbl ->
SmtAtom.Atom.reify_tbl ->
SmtAtom.Form.reify ->
- Environ.env -> Evd.evar_map -> Term.constr -> Proof_type.tactic
+ Environ.env -> Evd.evar_map -> Term.constr -> Structures.tactic
val tactic :
(SmtAtom.Btype.reify_tbl ->
SmtAtom.Op.reify_tbl ->
@@ -89,4 +89,4 @@ val tactic :
int * SmtAtom.Form.t SmtCertif.clause) ->
SmtAtom.Btype.reify_tbl ->
SmtAtom.Op.reify_tbl ->
- SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> Proof_type.tactic
+ SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> Structures.tactic