diff options
| author | letouzey | 2009-11-16 16:52:32 +0000 |
|---|---|---|
| committer | letouzey | 2009-11-16 16:52:32 +0000 |
| commit | df89fbc8ac8d0d485c1a373cb4edbb1835e2c4ad (patch) | |
| tree | bb0350ce29d299cd7b386667cba8a3fc327d4aa0 /plugins/interface | |
| parent | 8d7e3dc633eef34e0e806c4290aebf1b5a8d753d (diff) | |
New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))
"Module M (...) := M1 <+ M2 <+ M3 <+ ..." is now a shortcut for
"Module M (...). Include M1. Include M2. Include M3... End M."
Moreover M2,M3,etc can be functors as long as they find what they need in what
comes before them (see new command "Include Self").
The only real constraint is that M1,M2,M3,... should not have common elements
(for the moment (?)).
Same behavior for signature : Module Type M := M1 <+ M2 <+ M3.
Note that this <+ is _not_ a primitive construct of the module language,
for instance it cannot be used in signature (Module M <: M1 <+ M2 is
illegal for the moment).
Some example of use in Decidable2 and NZAxioms
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12530 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/interface')
| -rw-r--r-- | plugins/interface/xlate.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml index 7b35f4021b..97ab9efc88 100644 --- a/plugins/interface/xlate.ml +++ b/plugins/interface/xlate.ml @@ -2038,19 +2038,21 @@ let rec xlate_vernac = CT_module_type_decl(xlate_ident id, xlate_module_binder_list bl, match mty_o with - None -> + [] -> CT_coerce_ID_OPT_to_MODULE_TYPE_OPT ctv_ID_OPT_NONE - | Some mty1 -> + | [mty1] -> CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT - (xlate_module_type mty1)) + (xlate_module_type mty1) + | _ -> failwith "TODO: Include Self") | 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) + [] -> CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE + | [m] -> xlate_module_expr m + | _ -> failwith "TODO Include Self") | VernacDeclareModule(_,(_, id), bl, mty_o) -> CT_declare_module(xlate_ident id, xlate_module_binder_list bl, |