From fe570f948ce85c300a3677fe600215d2924905cb Mon Sep 17 00:00:00 2001 From: sacerdot Date: Thu, 6 Jan 2005 13:04:36 +0000 Subject: - Module/Declare Module syntax made more uniform: * "Module X [binders] [:T] [:= b]." is now used to define a module both in module definitions and module type definitions. Moreover "b" can now be a functor application in every situation (this was not accepted for module definitions in module type definitions) * "Declare Module X : T." is now used to declare a module both in module definitions and module type definitions. - Added syntactic sugar "Declare Module Export/Import" and "Module Export/Import" - Added syntactic sugar "Module M(Export/Import X Y: T)" and "Module Type M(Export/Import X Y: T)" (only for interactive definitions) (doc TODO) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6564 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/interface/xlate.ml | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) (limited to 'contrib') diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index e9e4a1560..ea1484d00 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1517,7 +1517,7 @@ let rec xlate_module_type = function let xlate_module_binder_list (l:module_binder list) = CT_module_binder_list - (List.map (fun (idl, mty) -> + (List.map (fun (_, idl, mty) -> let idl1 = List.map (fun (_, x) -> CT_ident (string_of_id x)) idl in let fst,idl2 = match idl1 with @@ -1915,20 +1915,18 @@ let rec xlate_vernac = | Some mty1 -> CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT (xlate_module_type mty1)) - | VernacDefineModule((_, id), bl, mty_o, mexpr_o) -> + | VernacDefineModule(_,(_, id), bl, mty_o, mexpr_o) -> CT_module(xlate_ident id, xlate_module_binder_list bl, xlate_module_type_check_opt mty_o, match mexpr_o with None -> CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE | Some m -> xlate_module_expr m) - | VernacDeclareModule((_, id), bl, mty_o, mexpr_o) -> + | VernacDeclareModule(_,(_, id), bl, mty_o) -> CT_declare_module(xlate_ident id, xlate_module_binder_list bl, - xlate_module_type_check_opt mty_o, - match mexpr_o with - None -> CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE - | Some m -> xlate_module_expr m) + xlate_module_type_check_opt (Some mty_o), + CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE) | VernacRequire (impexp, spec, id::idl) -> let ct_impexp, ct_spec = get_require_flags impexp spec in CT_require (ct_impexp, ct_spec, -- cgit v1.2.3