blob: b92ac3a0ec93919c30d86c0922fd6e1a235e28da (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
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 ->
Proof_global.t option
|
