aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/interface/blast.mli
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface/blast.mli')
-rw-r--r--contrib/interface/blast.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/interface/blast.mli b/contrib/interface/blast.mli
index e8bcf95c6..21c29bc98 100644
--- a/contrib/interface/blast.mli
+++ b/contrib/interface/blast.mli
@@ -1,5 +1,5 @@
-val blast_tac : (Ctast.t -> 'a) ->
- Proof_type.tactic_arg list ->
+val blast_tac : (Tacexpr.raw_tactic_expr -> 'a) ->
+ int list ->
Proof_type.goal Tacmach.sigma ->
Proof_type.goal list Proof_type.sigma * Proof_type.validation;;