blob: 2612f2b63e20f20270243e8ed0d6d2fb94c1492b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
open Constr
val tclUSER_if_not_mes :
unit Proofview.tactic
-> bool
-> Names.Id.t list option
-> unit Proofview.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
-> Declare.Proof.t option
|
