blob: a0d2fb2b9e91f2cc0dcec845cda1a906a823eca7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
val require_library : string -> unit
val subtac_one_fixpoint :
'a ->
'b ->
(Names.identifier * (int * Topconstr.recursion_order_expr) *
Topconstr.local_binder list * Topconstr.constr_expr *
Topconstr.constr_expr) *
'c ->
(Names.identifier * (int * Topconstr.recursion_order_expr) *
Topconstr.local_binder list * Topconstr.constr_expr *
Topconstr.constr_expr) *
'c
val subtac_fixpoint : 'a -> 'b -> unit
val subtac : Util.loc * Vernacexpr.vernac_expr -> unit
|
