blob: 07f151697ab3260997064c520843049410b7e907 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
open Util
type obligation_info = (Names.identifier * Term.types * Intset.t) array
val add_definition : Names.identifier -> Term.constr -> Term.types ->
obligation_info -> unit
val add_mutual_definitions :
(Names.identifier * int * Term.constr * Term.types * obligation_info) list -> unit
val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr option -> unit
val solve_obligations : Names.identifier option -> Proof_type.tactic -> unit
val show_obligations : Names.identifier option -> unit
|
