diff options
Diffstat (limited to 'contrib/cc/ccproof.mli')
-rw-r--r-- | contrib/cc/ccproof.mli | 31 |
1 files changed, 0 insertions, 31 deletions
diff --git a/contrib/cc/ccproof.mli b/contrib/cc/ccproof.mli deleted file mode 100644 index 0eb97efe..00000000 --- a/contrib/cc/ccproof.mli +++ /dev/null @@ -1,31 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id: ccproof.mli 9857 2007-05-24 14:21:08Z corbinea $ *) - -open Ccalgo -open Names -open Term - -type rule= - Ax of constr - | SymAx of constr - | Refl of term - | Trans of proof*proof - | Congr of proof*proof - | Inject of proof*constructor*int*int -and proof = - private {p_lhs:term;p_rhs:term;p_rule:rule} - -val build_proof : - forest -> - [ `Discr of int * pa_constructor * int * pa_constructor - | `Prove of int * int ] -> proof - - - |