diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-16 16:52:32 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-16 16:52:32 +0000 |
| commit | df89fbc8ac8d0d485c1a373cb4edbb1835e2c4ad (patch) | |
| tree | bb0350ce29d299cd7b386667cba8a3fc327d4aa0 /interp/topconstr.mli | |
| 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 'interp/topconstr.mli')
| -rw-r--r-- | interp/topconstr.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 1966bf552..1b6514a65 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -256,8 +256,8 @@ type module_type_ast = | CMTEwith of module_type_ast * with_declaration_ast type include_ast = - | CIMTE of module_type_ast - | CIME of module_ast + | CIMTE of module_type_ast * module_type_ast list + | CIME of module_ast * module_ast list val ntn_loc : Util.loc -> constr_expr notation_substitution -> string -> int val patntn_loc : Util.loc -> cases_pattern_expr notation_substitution -> string -> int |