blob: e6aa452defdc567ca44e2967a796ba67cdf8c0d9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
open Constr
val tclUSER_if_not_mes :
Tacmach.tactic ->
bool ->
Names.Id.t list option ->
Tacmach.tactic
val recursive_definition
: interactive_proof:bool
-> is_mes: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
-> Lemmas.t option
|
