summaryrefslogtreecommitdiff
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, 1 insertions, 3 deletions
diff --git a/contrib/interface/blast.mli b/contrib/interface/blast.mli
index 21c29bc9..f6701943 100644
--- a/contrib/interface/blast.mli
+++ b/contrib/interface/blast.mli
@@ -1,5 +1,3 @@
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;;
+ int list -> Proof_type.tactic