blob: 3225411c85d6f2b3622ac39cf62b68f7d464b78b (
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
: 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
-> Lemmas.t option
|
