Réforme de l'interprétation des termes :

- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t"
- "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième
  pretty-printer dans ppconstr.ml est basé sur "constr_expr".
- Nouveau répertoire "interp" qui hérite de la partie interprétation qui
  se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml;
  constrextern.ml est l'équivalent de termast.ml pour le nouveau
  printer; topconstr.ml; contient la définition de "constr_expr";
  modintern.ml remplace astmod.ml)
- Libnames.reference tend à remplacer Libnames.qualid


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

1 files changed, 2 insertions, 1 deletions

diff --git a/contrib/correctness/ptyping.mli b/contrib/correctness/ptyping.mli
index bfb7a9a86..968f4fd31 100644
--- a/contrib/correctness/ptyping.mli
+++ b/contrib/correctness/ptyping.mli
@@ -12,6 +12,7 @@
 
 open Names
 open Term
+open Topconstr
 
 open Ptype
 open Past
@@ -19,7 +20,7 @@ open Penv
 
 (* This module realizes type and effect inference *)
 
-val cic_type_v : local_env -> Prename.t -> Coqast.t ml_type_v -> type_v
+val cic_type_v : local_env -> Prename.t -> constr_expr ml_type_v -> type_v
 
 val effect_app : Prename.t -> local_env
             -> (typing_info,'b) Past.t