1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: ccproof.mli 9857 2007-05-24 14:21:08Z corbinea $ *)
19
| Trans of proof*proof
20
| Congr of proof*proof
21
| Inject of proof*constructor*int*int
23
private {p_lhs:term;p_rhs:term;p_rule:rule}
27
[ `Discr of int * pa_constructor * int * pa_constructor
28
| `Prove of int * int ] -> proof