summaryrefslogtreecommitdiff
path: root/contrib/subtac/subtac_obligations.mli
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
commit208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch)
tree591e9e512063e34099782e2518573f15ffeac003 /contrib/subtac/subtac_obligations.mli
parentde0085539583f59dc7c4bf4e272e18711d565466 (diff)
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'contrib/subtac/subtac_obligations.mli')
-rw-r--r--contrib/subtac/subtac_obligations.mli10
1 files changed, 10 insertions, 0 deletions
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
new file mode 100644
index 00000000..7d93d57b
--- /dev/null
+++ b/contrib/subtac/subtac_obligations.mli
@@ -0,0 +1,10 @@
+open Util
+
+val add_entry : Names.identifier -> Term.constr -> Term.types ->
+ (Names.identifier * Term.types * Intset.t) array -> unit
+
+val subtac_obligation : int * Names.identifier option -> unit
+
+val solve_obligations : Names.identifier option -> Proof_type.tactic -> unit
+
+val show_obligations : Names.identifier option -> unit