diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-01-06 13:04:36 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-01-06 13:04:36 +0000 |
| commit | fe570f948ce85c300a3677fe600215d2924905cb (patch) | |
| tree | b4864895bfe9be3a05ed1e670610512338570f1d /contrib | |
| parent | 842c86fd96b02b757cf47f57f4eb888fe40e10f4 (diff) | |
- 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
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/interface/xlate.ml | 12 |
1 files changed, 5 insertions, 7 deletions
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, |