mise en place de Correctness (ne compile pas encore)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1501 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 35 insertions, 0 deletions

diff --git a/contrib/correctness/ptyping.mli b/contrib/correctness/ptyping.mli
new file mode 100644
index 000000000..985d7b52e
--- /dev/null
+++ b/contrib/correctness/ptyping.mli
@@ -0,0 +1,35 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \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$ *)
+
+open Names
+open Term
+
+open Ptype
+open Past
+open Penv
+
+(* This module realizes type and effect inference *)
+
+val cic_type_v : local_env -> Renamings.t -> CoqAst.t ml_type_v -> type_v
+
+val effect_app : Renamings.t -> local_env
+            -> (typing_info,'b) ProgAst.t
+            -> (typing_info,constr) arg list
+            -> (type_v binder list * type_c) 
+             * ((identifier*identifier) list * (identifier*constr) list * bool)
+             * type_c
+
+val typed_var : Renamings.t -> local_env -> constr * constr -> variant
+
+val type_of_expression : Renamings.t -> local_env -> constr -> constr
+
+val states : Renamings.t -> local_env -> program -> typed_program