From 7acb63cad5f92c2618f99ca2a812a465092a523f Mon Sep 17 00:00:00 2001
From: soubiran
Date: Fri, 1 Feb 2008 12:18:37 +0000
Subject: Beaoucoup de changements dans la representation interne des modules.

kernel:

-declaration.ml
   unification des representations pour les modules et modules types.
     (type struct_expr_body)

-mod_typing.ml
   le typage des modules est separe de l'evaluation des modules

-modops.ml
   nouvelle fonction qui pour toutes expressions de structure calcule
   sa forme evaluee.(eval_struct)

-safe_typing.ml
  ajout du support du nouvel operateur Include.(add_include).


library:

-declaremods.ml
   nouveaux objets Include et Module-alias et gestion de la resolution de noms pour
   les alias via la nametab.

parsing:

-g_vernac.ml4:
   nouvelles regles pour le support des Includes et pour l'application des signatures
   fonctorielles.


extraction:
  Adaptation a la nouvelle representation des modules et support de l'operateur with.




git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10497 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/xlate.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'contrib/interface')

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index c261d57e97..0fbfa39b72 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1574,7 +1574,9 @@ let rec xlate_module_type = function
 	   | CWith_Module((_, idl), (_, qid)) ->
 	       CT_module_type_with_mod(mty1,
 				       CT_id_list (List.map xlate_ident idl), 
-				       CT_ident (xlate_qualid qid)));;
+				       CT_ident (xlate_qualid qid)))
+  | CMTEapply (_,_) -> xlate_error "TODO: Funsig application";;
+
 
 let xlate_module_binder_list (l:module_binder list) =
   CT_module_binder_list
@@ -1967,7 +1969,8 @@ let rec xlate_vernac =
    | VernacSyntacticDefinition (id, c, true, _) ->
        xlate_error "TODO: Local abbreviations"
   (* Modules and Module Types *)
-  | VernacDeclareModuleType((_, id), bl, mty_o)  -> 
+   | VernacInclude (_) -> xlate_error "TODO : Include "
+   | VernacDeclareModuleType((_, id), bl, mty_o)  -> 
       CT_module_type_decl(xlate_ident id,
 			  xlate_module_binder_list bl,
 			  match mty_o with
-- 
cgit v1.2.3