Module Cc_plugin.Ccproof

type rule =
| Ax of Ccalgo.axiom
| SymAx of Ccalgo.axiom
| 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;
}

Main proof building function

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