1 files changed, 0 insertions, 73 deletions
diff --git a/contrib/correctness/ptype.mli b/contrib/correctness/ptype.mli
deleted file mode 100644
index be181bcc..00000000
--- a/contrib/correctness/ptype.mli
+++ /dev/null
@@ -1,73 +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        *)
-(************************************************************************)
-
-(* Certification of Imperative Programs / Jean-Christophe Filliâtre *)
-
-(* $Id: ptype.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
-
-open Term
-
-(* Types des valeurs (V) et des calculs (C).
- *
- * On a C = r:V,E,P,Q 
- *
- *   et V = (x1:V1)...(xn:Vn)C | V ref | V array | <type pur>
- *
- * INVARIANT: l'effet E contient toutes les variables apparaissant dans
- *            le programme ET les annotations P et Q
- *            Si E = { x1,...,xn | y1,...,ym }, les variables x sont les
- *            variables en lecture seule et y1 les variables modifiées
- *            les xi sont libres dans P et Q, et les yi,result liées dans Q
- *            i.e.  P = p(x)
- *               et Q = [y1]...[yn][res]q(x,y,res)
- *)
-
-(* pre and post conditions *)
-
-type 'a precondition = { p_assert : bool; p_name : Names.name; p_value : 'a }
-
-type 'a assertion  = { a_name : Names.name; a_value : 'a }
-
-type 'a postcondition = 'a assertion
-
-type predicate = constr assertion
-
-(* binders *)
-
-type 'a binder_type =
-    BindType  of 'a
-  | BindSet
-  | Untyped
-
-type 'a binder = Names.identifier * 'a binder_type
-
-(* variant *)
-
-type variant = constr * constr * constr (* phi, R, A *)
-
-(* types des valeurs *)
-
-type 'a ml_type_v =
-    Ref       of 'a ml_type_v
-  | Array     of 'a * 'a ml_type_v   (* size x type *)
-  | Arrow     of 'a ml_type_v binder list * 'a ml_type_c
-
-  | TypePure  of 'a
-
-(* et type des calculs *)
-
-and 'a ml_type_c =
-    (Names.identifier * 'a ml_type_v) 
-  * Peffect.t
-  * ('a precondition list) * ('a postcondition option)
-
-(* at beginning they contain Coq AST but they become constr after typing *)
-type type_v = constr ml_type_v
-type type_c = constr ml_type_c
-
-