Module Cc_plugin.Ccproof
type rule
=
|
Ax of Constr.constr
|
SymAx of Constr.constr
|
Refl of Ccalgo.ATerm.t
|
Trans of proof * proof
|
Congr of proof * proof
|
Inject of proof * Constr.pconstructor * int * int
and proof
= private
{
p_lhs : Ccalgo.ATerm.t;
p_rhs : Ccalgo.ATerm.t;
p_rule : rule;
}
val prefl : Ccalgo.ATerm.t -> proof
val pcongr : proof -> proof -> proof
val ptrans : proof -> proof -> proof
val psym : proof -> proof
val pax : (Ccalgo.ATerm.t * Ccalgo.ATerm.t) Cc_plugin.Ccalgo.Constrhash.t -> Cc_plugin.Ccalgo.Constrhash.key -> proof
val psymax : (Ccalgo.ATerm.t * Ccalgo.ATerm.t) Cc_plugin.Ccalgo.Constrhash.t -> Cc_plugin.Ccalgo.Constrhash.key -> proof
val pinject : proof -> Constr.pconstructor -> int -> int -> proof
val equal_proof : Environ.env -> Evd.evar_map -> Ccalgo.forest -> int -> int -> proof
val edge_proof : Environ.env -> Evd.evar_map -> Ccalgo.forest -> ((int * int) * Ccalgo.equality) -> proof
val path_proof : Environ.env -> Evd.evar_map -> Ccalgo.forest -> int -> ((int * int) * Ccalgo.equality) list -> proof
val congr_proof : Environ.env -> Evd.evar_map -> Ccalgo.forest -> int -> int -> proof
val ind_proof : Environ.env -> Evd.evar_map -> Ccalgo.forest -> int -> Ccalgo.pa_constructor -> int -> Ccalgo.pa_constructor -> proof
val build_proof : Environ.env -> Evd.evar_map -> Ccalgo.forest -> [ `Discr of int * Ccalgo.pa_constructor * int * Ccalgo.pa_constructor | `Prove of int * int ] -> proof