aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder/rules.mli
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder/rules.mli')
-rw-r--r--plugins/firstorder/rules.mli4
1 files changed, 3 insertions, 1 deletions
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index 381b7cd87..fb2173083 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -7,10 +7,12 @@
(************************************************************************)
open Term
-open Tacmach
+open EConstr
open Names
open Globnames
+type tactic = unit Proofview.tactic
+
type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
type lseqtac= global_reference -> seqtac