blob: 549f1fc0e48f4a4e5e7d777651121b3b70d02bfa (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
open Constr
val tclUSER_if_not_mes :
Tacmach.tactic ->
bool ->
Names.Id.t list option ->
Tacmach.tactic
val recursive_definition :
bool ->
Names.Id.t ->
Constrintern.internalization_env ->
Constrexpr.constr_expr ->
Constrexpr.constr_expr ->
int -> Constrexpr.constr_expr -> (pconstant ->
Indfun_common.tcc_lemma_value ref ->
pconstant ->
pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> unit
|
