blob: 7d93d57bb83983f944ac8b1db89e48a1d0430cf0 (
plain)
1
2
3
4
5
6
7
8
9
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
|
