diff options
30 files changed, 164 insertions, 162 deletions
@@ -91,6 +91,8 @@ Vernacular commands - Declaring axiomatic type class instances in Module Type should be now done via new command "Declare Instance", while the syntax "Instance" now always provides a concrete instance, both in and out of Module Type. +- Include Type is now deprecated since Include now accept both modules and + module types. Tools diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex index 4d213e1f2..40fd6f110 100644 --- a/doc/refman/RefMan-mod.tex +++ b/doc/refman/RefMan-mod.tex @@ -65,23 +65,17 @@ This command is used to start an interactive module named {\ident}. \subsubsection{Reserved commands inside an interactive module: \comindex{Include}} \begin{enumerate} -\item {\tt Include {\modexpr}} +\item {\tt Include {\module}} - Includes the content of {\modexpr} in the current interactive module type. If {\modexpr} is a high-order module expression then the system tries to instanciate {\modexpr} + Includes the content of {\module} in the current interactive + module. Here {\module} can be a module expresssion or a module type + expression. If {\module} is a high-order module or module type + expression then the system tries to instanciate {\module} by the current interactive module. -\item {\tt Include Type {\modtype}} +\item {\tt Include {\module$_1$} \verb.<+. $\ldots$ \verb.<+. {\module$_n$}} - Includes the content of {\modtype} in the current interactive module type. If {\modtype} is a high-order module type expression then the system tries to instanciate {\modtype} - by the current interactive module. - -\item {\tt Include {\modexpr$_1$} \verb.<+. $\ldots$ \verb.<+. {\modexpr$_n$}} - -is a shortcut for {\tt Include {\modexpr$_1$}} $\ldots$ {\tt Include {\modexpr$_n$}} - -\item {\tt Include Type {\modtype$_1$} \verb.<+. $\ldots$ \verb.<+. {\modtype$_n$}} - -is a shortcut for {\tt Include Type {\modtype$_1$}} $\ldots$ {\tt Include Type {\modtype$_n$}} +is a shortcut for {\tt Include {\module$_1$}} $\ldots$ {\tt Include {\module$_n$}} \end{enumerate} \subsection{\tt End {\ident} \comindex{End}} @@ -151,23 +145,13 @@ This command is used to start an interactive module type {\ident}. \subsubsection{Reserved commands inside an interactive module type: \comindex{Include}\comindex{Inline}} \begin{enumerate} -\item {\tt Include {\modexpr}} - - Includes the content of {\modexpr} in the current interactive module type. If {\modexpr} is a high-order module expression then the system tries to instanciate {\modexpr} - by the current interactive module type. - -\item {\tt Include Type {\modtype}} - - Includes the content of {\modtype} in the current interactive module type. If {\modtype} is a high-order module type expression then the system tries to instanciate {\modtype} - by the current interactive module type. - -\item {\tt Include {\modexpr$_1$} \verb.<+. $\ldots$ \verb.<+. {\modexpr$_n$}} +\item {\tt Include {\module}} -is a shortcut for {\tt Include {\modexpr$_1$}} $\ldots$ {\tt Include {\modexpr$_n$}} + Same as {\tt Include} inside a module. -\item {\tt Include Type {\modtype$_1$} \verb.<+. $\ldots$ \verb.<+. {\modtype$_n$}} +\item {\tt Include {\module$_1$} \verb.<+. $\ldots$ \verb.<+. {\module$_n$}} -is a shortcut for {\tt Include Type {\modtype$_1$}} $\ldots$ {\tt Include Type {\modtype$_n$}} +is a shortcut for {\tt Include {\module$_1$}} $\ldots$ {\tt Include {\module$_n$}} \item {\tt {\declarationkeyword} Inline {\assums} } diff --git a/interp/modintern.ml b/interp/modintern.ml index 041e32bf6..049745ca9 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -80,6 +80,16 @@ let lookup_modtype (loc,qid) = | Not_found -> Modops.error_not_a_modtype_loc loc (string_of_qualid qid) +let lookup_module_or_modtype (loc,qid) = + try + let mp = Nametab.locate_module qid in + Dumpglob.dump_modref loc mp "modtype"; (mp,true) + with Not_found -> try + let mp = Nametab.locate_modtype qid in + Dumpglob.dump_modref loc mp "mod"; (mp,false) + with Not_found -> + Modops.error_not_a_module_or_modtype_loc loc (string_of_qualid qid) + let transl_with_decl env = function | CWith_Module ((_,fqid),qid) -> With_Module (fqid,lookup_module qid) @@ -87,22 +97,38 @@ let transl_with_decl env = function With_Definition (fqid,interp_constr Evd.empty env c) let rec interp_modexpr env = function - | CMEident qid -> + | CMident qid -> MSEident (lookup_module qid) - | CMEapply (me1,me2) -> + | CMapply (me1,me2) -> let me1 = interp_modexpr env me1 in let me2 = interp_modexpr env me2 in MSEapply(me1,me2) + | CMwith _ -> Modops.error_with_in_module () + let rec interp_modtype env = function - | CMTEident qid -> + | CMident qid -> MSEident (lookup_modtype qid) - | CMTEapply (mty1,me) -> + | CMapply (mty1,me) -> let mty' = interp_modtype env mty1 in let me' = interp_modexpr env me in MSEapply(mty',me') - | CMTEwith (mty,decl) -> + | CMwith (mty,decl) -> let mty = interp_modtype env mty in let decl = transl_with_decl env decl in MSEwith(mty,decl) +let rec interp_modexpr_or_modtype env = function + | CMident qid -> + let (mp,ismod) = lookup_module_or_modtype qid in + (MSEident mp, ismod) + | CMapply (me1,me2) -> + let me1,ismod1 = interp_modexpr_or_modtype env me1 in + let me2,ismod2 = interp_modexpr_or_modtype env me2 in + if not ismod2 then Modops.error_application_to_module_type (); + (MSEapply (me1,me2), ismod1) + | CMwith (me,decl) -> + let me,ismod = interp_modexpr_or_modtype env me in + let decl = transl_with_decl env decl in + if ismod then Modops.error_with_in_module (); + (MSEwith(me,decl), ismod) diff --git a/interp/modintern.mli b/interp/modintern.mli index f39205d8b..e528b7af7 100644 --- a/interp/modintern.mli +++ b/interp/modintern.mli @@ -21,8 +21,15 @@ open Topconstr (* Module expressions and module types are interpreted relatively to eventual functor or funsig arguments. *) -val interp_modtype : env -> module_type_ast -> module_struct_entry +val interp_modtype : env -> module_ast -> module_struct_entry val interp_modexpr : env -> module_ast -> module_struct_entry +(* The following function tries to interprete an ast as a module, + and in case of failure, interpretes this ast as a module type. + The boolean is true for a module, false for a module type *) + +val interp_modexpr_or_modtype : env -> module_ast -> + module_struct_entry * bool + val lookup_module : qualid located -> module_path diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 155fd1c02..d93e1ab14 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -1005,17 +1005,9 @@ type with_declaration_ast = | CWith_Definition of identifier list located * constr_expr type module_ast = - | CMEident of qualid located - | CMEapply of module_ast * module_ast - -type module_type_ast = - | CMTEident of qualid located - | CMTEapply of module_type_ast * module_ast - | CMTEwith of module_type_ast * with_declaration_ast - -type include_ast = - | CIMTE of module_type_ast list - | CIME of module_ast list + | CMident of qualid located + | CMapply of module_ast * module_ast + | CMwith of module_ast * with_declaration_ast type 'a module_signature = | Enforce of 'a (* ... : T *) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 6e3951b2f..1b1698f95 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -242,17 +242,9 @@ type with_declaration_ast = | CWith_Definition of identifier list located * constr_expr type module_ast = - | CMEident of qualid located - | CMEapply of module_ast * module_ast - -type module_type_ast = - | CMTEident of qualid located - | CMTEapply of module_type_ast * module_ast - | CMTEwith of module_type_ast * with_declaration_ast - -type include_ast = - | CIMTE of module_type_ast list - | CIME of module_ast list + | CMident of qualid located + | CMapply of module_ast * module_ast + | CMwith of module_ast * with_declaration_ast type 'a module_signature = | Enforce of 'a (* ... : T *) diff --git a/kernel/modops.ml b/kernel/modops.ml index 8c014c1d7..000b2d65e 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -61,6 +61,9 @@ let error_not_a_modtype_loc loc s = let error_not_a_module_loc loc s = user_err_loc (loc,"",str ("\""^s^"\" is not a module.")) +let error_not_a_module_or_modtype_loc loc s = + user_err_loc (loc,"",str ("\""^s^"\" is not a module or module type.")) + let error_not_a_module s = error_not_a_module_loc dummy_loc s let error_not_a_constant l = @@ -86,6 +89,9 @@ let error_local_context lo = let error_no_such_label_sub l l1 = error ("The field "^(string_of_label l)^" is missing in "^l1^".") +let error_with_in_module _ = error "The syntax \"with\" is not allowed for modules." + +let error_application_to_module_type _ = error "Module application to a module type." let destr_functor env mtb = match mtb with diff --git a/kernel/modops.mli b/kernel/modops.mli index 44d29ee3e..435c196f9 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -84,6 +84,8 @@ val error_not_a_modtype_loc : loc -> string -> 'a val error_not_a_module_loc : loc -> string -> 'a +val error_not_a_module_or_modtype_loc : loc -> string -> 'a + val error_not_a_module : string -> 'a val error_not_a_constant : label -> 'a @@ -96,5 +98,7 @@ val error_local_context : label option -> 'a val error_no_such_label_sub : label->string->'a +val error_with_in_module : unit -> 'a +val error_application_to_module_type : unit -> 'a diff --git a/library/declaremods.ml b/library/declaremods.ml index 97047ebd7..5db0e0abc 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -897,9 +897,8 @@ let get_includeself_substobjs env objs me is_mod = ([],mp_self,subst_objects subst objects) with NothingToDo -> objs -let declare_one_include interp_struct me_ast is_mod = +let declare_one_include_inner (me,is_mod) = let env = Global.env() in - let me = interp_struct env me_ast in let mp1,_ = current_prefix () in let (mbids,mp,objs)= if is_mod then @@ -918,11 +917,11 @@ let declare_one_include interp_struct me_ast is_mod = ignore (add_leaf id (in_include ((me,is_mod), substobjs))) +let declare_one_include interp_struct me_ast = + declare_one_include_inner (interp_struct (Global.env()) me_ast) -let declare_include_ interp_struct me_asts is_mod = - List.iter - (fun me -> declare_one_include interp_struct me is_mod) - me_asts +let declare_include_ interp_struct me_asts = + List.iter (declare_one_include interp_struct) me_asts (** Versions of earlier functions taking care of the freeze/unfreeze of summaries *) @@ -934,17 +933,17 @@ let protect_summaries f = (* Something wrong: undo the whole process *) Summary.unfreeze_summaries fs; raise e -let declare_include interp_struct me_asts is_mod = +let declare_include interp_struct me_asts = protect_summaries - (fun _ -> declare_include_ interp_struct me_asts is_mod) + (fun _ -> declare_include_ interp_struct me_asts) -let declare_modtype interp_mt id args mtys mty_l = +let declare_modtype interp_mt interp_mix id args mtys mty_l = let declare_mt fs = match mty_l with | [] -> assert false | [mty] -> declare_modtype_ interp_mt id args mtys mty fs | mty_l -> ignore (start_modtype_ interp_mt id args mtys fs); - declare_include_ interp_mt mty_l false; + declare_include_ interp_mix mty_l; end_modtype () in protect_summaries declare_mt @@ -952,13 +951,13 @@ let declare_modtype interp_mt id args mtys mty_l = let start_modtype interp_modtype id args mtys = protect_summaries (start_modtype_ interp_modtype id args mtys) -let declare_module interp_mt interp_me id args mtys me_l = +let declare_module interp_mt interp_me interp_mix id args mtys me_l = let declare_me fs = match me_l with | [] -> declare_module_ interp_mt interp_me id args mtys None fs | [me] -> declare_module_ interp_mt interp_me id args mtys (Some me) fs | me_l -> ignore (start_module_ interp_mt None id args mtys fs); - declare_include_ interp_me me_l true; + declare_include_ interp_mix me_l; end_module () in protect_summaries declare_me diff --git a/library/declaremods.mli b/library/declaremods.mli index ae0b0aa10..1db3d95a8 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -37,16 +37,17 @@ open Lib *) val declare_module : - (env -> 'modtype -> module_struct_entry) -> - (env -> 'modexpr -> module_struct_entry) -> + (env -> 'modast -> module_struct_entry) -> + (env -> 'modast -> module_struct_entry) -> + (env -> 'modast -> module_struct_entry * bool) -> identifier -> - (identifier located list * 'modtype) list -> - 'modtype Topconstr.module_signature -> - 'modexpr list -> module_path + (identifier located list * 'modast) list -> + 'modast Topconstr.module_signature -> + 'modast list -> module_path -val start_module : (env -> 'modtype -> module_struct_entry) -> - bool option -> identifier -> (identifier located list * 'modtype) list -> - 'modtype Topconstr.module_signature -> module_path +val start_module : (env -> 'modast -> module_struct_entry) -> + bool option -> identifier -> (identifier located list * 'modast) list -> + 'modast Topconstr.module_signature -> module_path val end_module : unit -> module_path @@ -54,13 +55,14 @@ val end_module : unit -> module_path (*s Module types *) -val declare_modtype : (env -> 'modtype -> module_struct_entry) -> - identifier -> (identifier located list * 'modtype) list -> - 'modtype list -> 'modtype list -> module_path +val declare_modtype : (env -> 'modast -> module_struct_entry) -> + (env -> 'modast -> module_struct_entry * bool) -> + identifier -> (identifier located list * 'modast) list -> + 'modast list -> 'modast list -> module_path -val start_modtype : (env -> 'modtype -> module_struct_entry) -> - identifier -> (identifier located list * 'modtype) list -> - 'modtype list -> module_path +val start_modtype : (env -> 'modast -> module_struct_entry) -> + identifier -> (identifier located list * 'modast) list -> + 'modast list -> module_path val end_modtype : unit -> module_path @@ -103,8 +105,8 @@ val import_module : bool -> module_path -> unit (* Include *) -val declare_include : (env -> 'struct_expr -> module_struct_entry) -> - 'struct_expr list -> bool -> unit +val declare_include : (env -> 'struct_expr -> module_struct_entry * bool) -> + 'struct_expr list -> unit (*s [iter_all_segments] iterate over all segments, the modules' segments first and then the current segment. Modules are presented diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 4672a732a..f4d588b57 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -397,9 +397,10 @@ GEXTEND Gram | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl) | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) | IDENT "Include"; e = module_expr; l = LIST0 ext_module_expr -> - VernacInclude(CIME(e::l)) + VernacInclude(e::l) | IDENT "Include"; "Type"; e = module_type; l = LIST0 ext_module_type -> - VernacInclude(CIMTE(e::l)) ] ] + warning "Include Type is deprecated; use Include instead"; + VernacInclude(e::l) ] ] ; export_token: [ [ IDENT "Import" -> Some false @@ -440,11 +441,11 @@ GEXTEND Gram (* Module expressions *) module_expr: [ [ me = module_expr_atom -> me - | me1 = module_expr; me2 = module_expr_atom -> CMEapply (me1,me2) + | me1 = module_expr; me2 = module_expr_atom -> CMapply (me1,me2) ] ] ; module_expr_atom: - [ [ qid = qualid -> CMEident qid | "("; me = module_expr; ")" -> me ] ] + [ [ qid = qualid -> CMident qid | "("; me = module_expr; ")" -> me ] ] ; with_declaration: [ [ "Definition"; fqid = fullyqualid; ":="; c = Constr.lconstr -> @@ -454,10 +455,10 @@ GEXTEND Gram ] ] ; module_type: - [ [ qid = qualid -> CMTEident qid + [ [ qid = qualid -> CMident qid | "("; mt = module_type; ")" -> mt - | mty = module_type; me = module_expr_atom -> CMTEapply (mty,me) - | mty = module_type; "with"; decl = with_declaration -> CMTEwith (mty,decl) + | mty = module_type; me = module_expr_atom -> CMapply (mty,me) + | mty = module_type; "with"; decl = with_declaration -> CMwith (mty,decl) ] ] ; END diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index d724e2e73..6d5455b1b 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -214,7 +214,7 @@ module Constr : module Module : sig val module_expr : module_ast Gram.Entry.e - val module_type : module_type_ast Gram.Entry.e + val module_type : module_ast Gram.Entry.e end module Tactic : diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 4b1162dbd..92a455abc 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -234,29 +234,22 @@ let pr_with_declaration pr_c = function str"Module" ++ spc() ++ pr_lfqid id ++ str" := " ++ pr_located pr_qualid qid -let rec pr_module_type pr_c = function - | CMTEident qid -> spc () ++ pr_located pr_qualid qid - | CMTEwith (mty,decl) -> - let m = pr_module_type pr_c mty in +let rec pr_module_ast pr_c = function + | CMident qid -> spc () ++ pr_located pr_qualid qid + | CMwith (mty,decl) -> + let m = pr_module_ast pr_c mty in let p = pr_with_declaration pr_c decl in m ++ spc() ++ str"with" ++ spc() ++ p - | CMTEapply (fexpr,mexpr)-> - let f = pr_module_type pr_c fexpr in - let m = pr_module_expr mexpr in - f ++ spc () ++ m - -and pr_module_expr = function - | CMEident qid -> pr_located pr_qualid qid - | CMEapply (me1,(CMEident _ as me2)) -> - pr_module_expr me1 ++ spc() ++ pr_module_expr me2 - | CMEapply (me1,me2) -> - pr_module_expr me1 ++ spc() ++ - hov 1 (str"(" ++ pr_module_expr me2 ++ str")") + | CMapply (me1,(CMident _ as me2)) -> + pr_module_ast pr_c me1 ++ spc() ++ pr_module_ast pr_c me2 + | CMapply (me1,me2) -> + pr_module_ast pr_c me1 ++ spc() ++ + hov 1 (str"(" ++ pr_module_ast pr_c me2 ++ str")") let pr_of_module_type prc = function - | Enforce mty -> str ":" ++ pr_module_type prc mty + | Enforce mty -> str ":" ++ pr_module_ast prc mty | Check mtys -> - prlist_strict (fun m -> str "<:" ++ pr_module_type prc m) mtys + prlist_strict (fun m -> str "<:" ++ pr_module_ast prc m) mtys let pr_require_token = function | Some true -> str "Export " @@ -264,7 +257,7 @@ let pr_require_token = function | None -> mt() let pr_module_vardecls pr_c (export,idl,mty) = - let m = pr_module_type pr_c mty in + let m = pr_module_ast pr_c mty in (* Update the Nametab for interpreting the body of module/modtype *) let lib_dir = Lib.library_dp() in List.iter (fun (_,id) -> @@ -751,27 +744,24 @@ let rec pr_vernac = function pr_lident m ++ b ++ pr_of_module_type pr_lconstr tys ++ (if bd = [] then mt () else str ":= ") ++ - prlist_with_sep (fun () -> str " <+ ") pr_module_expr bd) + prlist_with_sep (fun () -> str " <+ ") + (pr_module_ast pr_lconstr) bd) | VernacDeclareModule (export,id,bl,m1) -> let b = pr_module_binders_list bl pr_lconstr in hov 2 (str"Declare Module" ++ spc() ++ pr_require_token export ++ pr_lident id ++ b ++ - pr_module_type pr_lconstr m1) + pr_module_ast pr_lconstr m1) | VernacDeclareModuleType (id,bl,tyl,m) -> let b = pr_module_binders_list bl pr_lconstr in - let pr_mt = pr_module_type pr_lconstr in + let pr_mt = pr_module_ast pr_lconstr in hov 2 (str"Module Type " ++ pr_lident id ++ b ++ prlist_strict (fun m -> str " <: " ++ pr_mt m) tyl ++ (if m = [] then mt () else str ":= ") ++ prlist_with_sep (fun () -> str " <+ ") pr_mt m) - | VernacInclude (CIMTE(mtys)) -> - let pr_mty = pr_module_type pr_lconstr in - hov 2 (str"Include Type " ++ - prlist_with_sep (fun () -> str " <+ ") pr_mty mtys) - | VernacInclude (CIME(mexprs)) -> - let pr_me = pr_module_expr in + | VernacInclude (mexprs) -> + let pr_m = pr_module_ast pr_lconstr in hov 2 (str"Include " ++ - prlist_with_sep (fun () -> str " <+ ") pr_me mexprs) + prlist_with_sep (fun () -> str " <+ ") pr_m mexprs) (* Solving *) | VernacSolve (i,tac,deftac) -> (if i = 1 then mt() else int i ++ str ": ") ++ diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v index cd51b2aff..e60cca9d9 100644 --- a/theories/FSets/FMapInterface.v +++ b/theories/FSets/FMapInterface.v @@ -258,7 +258,7 @@ End WSfun. Module Type WS. Declare Module E : DecidableType. - Include Type WSfun E. + Include WSfun E. End WS. @@ -266,7 +266,7 @@ End WS. (** ** Maps on ordered keys, functorial signature *) Module Type Sfun (E : OrderedType). - Include Type WSfun E. + Include WSfun E. Section elt. Variable elt:Type. Definition lt_key (p p':key*elt) := E.lt (fst p) (fst p'). @@ -284,7 +284,7 @@ End Sfun. Module Type S. Declare Module E : OrderedType. - Include Type Sfun E. + Include Sfun E. End S. diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v index d94ff7c95..8aede5527 100644 --- a/theories/FSets/FSetInterface.v +++ b/theories/FSets/FSetInterface.v @@ -275,7 +275,7 @@ End WSfun. Module Type WS. Declare Module E : DecidableType. - Include Type WSfun E. + Include WSfun E. End WS. @@ -286,7 +286,7 @@ End WS. and some stronger specifications for other functions. *) Module Type Sfun (E : OrderedType). - Include Type WSfun E. + Include WSfun E. Parameter lt : t -> t -> Prop. Parameter compare : forall s s' : t, Compare lt eq s s'. @@ -349,7 +349,7 @@ End Sfun. Module Type S. Declare Module E : OrderedType. - Include Type Sfun E. + Include Sfun E. End S. diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v index effd5e35a..cb18785e6 100644 --- a/theories/MSets/MSetInterface.v +++ b/theories/MSets/MSetInterface.v @@ -117,7 +117,7 @@ End HasWOps. Module Type WOps (E : DecidableType). Definition elt := E.t. Parameter t : Type. (** the abstract type of sets *) - Include Type HasWOps. + Include HasWOps. End WOps. @@ -128,7 +128,7 @@ End WOps. Module Type WSetsOn (E : DecidableType). (** First, we ask for all the functions *) - Include Type WOps E. + Include WOps E. (** Logical predicates *) Parameter In : elt -> t -> Prop. @@ -144,8 +144,8 @@ Module Type WSetsOn (E : DecidableType). Notation "s [<=] t" := (Subset s t) (at level 70, no associativity). Definition eq : t -> t -> Prop := Equal. - Include Type IsEq. (** [eq] is obviously an equivalence, for subtyping only *) - Include Type HasEqDec. + Include IsEq. (** [eq] is obviously an equivalence, for subtyping only *) + Include HasEqDec. (** Specifications of set operators *) @@ -197,7 +197,7 @@ End WSetsOn. Module Type WSets. Declare Module E : DecidableType. - Include Type WSetsOn E. + Include WSetsOn E. End WSets. (** ** Functorial signature for sets on ordered elements @@ -226,7 +226,7 @@ Module Type Ops (E : OrderedType) := WOps E <+ HasOrdOps. Module Type SetsOn (E : OrderedType). - Include Type WSetsOn E <+ HasOrdOps <+ HasLt <+ IsStrOrder. + Include WSetsOn E <+ HasOrdOps <+ HasLt <+ IsStrOrder. Section Spec. Variable s s': t. @@ -266,7 +266,7 @@ End SetsOn. Module Type Sets. Declare Module E : OrderedType. - Include Type SetsOn E. + Include SetsOn E. End Sets. Module Type S := Sets. @@ -335,7 +335,7 @@ Module WS_WSfun (M : WSets) <: WSetsOn M.E := M. Module Type WRawSets (E : DecidableType). (** First, we ask for all the functions *) - Include Type WOps E. + Include WOps E. (** Is a set well-formed or ill-formed ? *) @@ -559,7 +559,7 @@ End WRaw2Sets. (** Same approach for ordered sets *) Module Type RawSets (E : OrderedType). - Include Type WRawSets E <+ HasOrdOps <+ HasLt <+ IsStrOrder. + Include WRawSets E <+ HasOrdOps <+ HasLt <+ IsStrOrder. Section Spec. Variable s s': t. diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v index 9b5a80762..44bb02ecc 100644 --- a/theories/Numbers/Integer/Abstract/ZBase.v +++ b/theories/Numbers/Integer/Abstract/ZBase.v @@ -15,7 +15,7 @@ Require Export ZAxioms. Require Import NZProperties. Module ZBasePropFunct (Import Z : ZAxiomsSig'). -Include Type NZPropFunct Z. +Include NZPropFunct Z. (* Theorems that are true for integers but not for natural numbers *) diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v index 7f2253205..9b6f0ff64 100644 --- a/theories/Numbers/Integer/Abstract/ZProperties.v +++ b/theories/Numbers/Integer/Abstract/ZProperties.v @@ -18,6 +18,6 @@ Require Export ZAxioms ZMulOrder. Module Type ZPropSig := ZMulOrderPropFunct. Module ZPropFunct (Z:ZAxiomsSig) <: ZPropSig Z. - Include Type ZPropSig Z. + Include ZPropSig Z. End ZPropFunct. diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v index 7313c4131..97c122029 100644 --- a/theories/Numbers/NatInt/NZAddOrder.v +++ b/theories/Numbers/NatInt/NZAddOrder.v @@ -13,7 +13,7 @@ Require Import NZAxioms NZBase NZMul NZOrder. Module Type NZAddOrderPropSig (Import NZ : NZOrdAxiomsSig'). -Include Type NZBasePropSig NZ <+ NZMulPropSig NZ <+ NZOrderPropSig NZ. +Include NZBasePropSig NZ <+ NZMulPropSig NZ <+ NZOrderPropSig NZ. Theorem add_lt_mono_l : forall n m p, n < m <-> p + n < p + m. Proof. diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v index 3c11024e5..296bd095f 100644 --- a/theories/Numbers/NatInt/NZMul.v +++ b/theories/Numbers/NatInt/NZMul.v @@ -14,7 +14,7 @@ Require Import NZAxioms NZBase NZAdd. Module Type NZMulPropSig (Import NZ : NZAxiomsSig')(Import NZBase : NZBasePropSig NZ). -Include Type NZAddPropSig NZ NZBase. +Include NZAddPropSig NZ NZBase. Theorem mul_0_r : forall n, n * 0 == 0. Proof. diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v index 18f61de59..7b64a6983 100644 --- a/theories/Numbers/NatInt/NZMulOrder.v +++ b/theories/Numbers/NatInt/NZMulOrder.v @@ -14,7 +14,7 @@ Require Import NZAxioms. Require Import NZAddOrder. Module Type NZMulOrderPropSig (Import NZ : NZOrdAxiomsSig'). -Include Type NZAddOrderPropSig NZ. +Include NZAddOrderPropSig NZ. Theorem mul_lt_pred : forall p q n m, S p == q -> (p * n < p * m <-> q * n + m < q * m + n). diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index 6697c0b3d..6a086f3bd 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -611,7 +611,6 @@ End WF. End NZOrderPropSig. -Module NZOrderPropFunct (Import NZ : NZOrdSig). - Include Type NZBasePropSig NZ <+ NZOrderPropSig NZ. -End NZOrderPropFunct. +Module NZOrderPropFunct (NZ : NZOrdSig) := + NZBasePropSig NZ <+ NZOrderPropSig NZ. diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index 0d489a16d..842f4bcf2 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -16,7 +16,7 @@ Require Import NZProperties. Module NBasePropFunct (Import N : NAxiomsSig'). (** First, we import all known facts about both natural numbers and integers. *) -Include Type NZPropFunct N. +Include NZPropFunct N. (** We prove that the successor of a number is not zero by defining a function (by recursion) that maps 0 to false and the successor to true *) diff --git a/theories/Numbers/Natural/Abstract/NProperties.v b/theories/Numbers/Natural/Abstract/NProperties.v index 2baed54cf..30262bd9f 100644 --- a/theories/Numbers/Natural/Abstract/NProperties.v +++ b/theories/Numbers/Natural/Abstract/NProperties.v @@ -18,5 +18,5 @@ Require Export NAxioms NSub. Module Type NPropSig := NSubPropFunct. Module NPropFunct (N:NAxiomsSig) <: NPropSig N. - Include Type NPropSig N. + Include NPropSig N. End NPropFunct. diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v index ed867b825..cbbcdbff5 100644 --- a/theories/Numbers/Natural/Abstract/NStrongRec.v +++ b/theories/Numbers/Natural/Abstract/NStrongRec.v @@ -16,7 +16,7 @@ and proves its properties *) Require Export NSub. Module NStrongRecPropFunct (Import N : NAxiomsSig'). -Include Type NSubPropFunct N. +Include NSubPropFunct N. Section StrongRecursion. diff --git a/theories/Structures/OrderTac.v b/theories/Structures/OrderTac.v index 43df377c0..2465dc539 100644 --- a/theories/Structures/OrderTac.v +++ b/theories/Structures/OrderTac.v @@ -53,7 +53,7 @@ Local Infix "+" := trans_ord. Module Type TotalOrder_NoInline <: TotalOrder. Parameter Inline t : Type. Parameters eq lt le : t -> t -> Prop. - Include Type IsEq <+ IsStrOrder <+ LeIsLtEq <+ LtIsTotal. + Include IsEq <+ IsStrOrder <+ LeIsLtEq <+ LtIsTotal. End TotalOrder_NoInline. Module Type TotalOrder_NoInline' := TotalOrder_NoInline <+ EqLtLeNotation. @@ -302,7 +302,7 @@ Definition t := O.t. Definition eq := O.eq. Definition lt := flip O.lt. Definition le := flip O.le. -Include Type EqLtLeNotation. +Include EqLtLeNotation. Instance eq_equiv : Equivalence eq. diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index ca441fc86..1f3e50dc3 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -41,7 +41,7 @@ Module Type MiniOrderedType. End MiniOrderedType. Module Type OrderedType. - Include Type MiniOrderedType. + Include MiniOrderedType. (** A [eq_dec] can be deduced from [compare] below. But adding this redundant field allows to see an OrderedType as a DecidableType. *) diff --git a/theories/Structures/OrderedType2.v b/theories/Structures/OrderedType2.v index 1cddfea3b..766b0faf0 100644 --- a/theories/Structures/OrderedType2.v +++ b/theories/Structures/OrderedType2.v @@ -43,7 +43,7 @@ Module Type LeNotation (E:EqLe). End LeNotation. Module Type LtLeNotation (E:EqLtLe). - Include Type LtNotation E <+ LeNotation E. + Include LtNotation E <+ LeNotation E. Notation "x <= y < z" := (x<=y /\ y<z). Notation "x < y <= z" := (x<y /\ y<=z). End LtLeNotation. diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 7955d4916..b56b0b26f 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -453,6 +453,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast = else (idl,ty)) binders_ast in let mp = Declaremods.declare_module Modintern.interp_modtype Modintern.interp_modexpr + Modintern.interp_modexpr_or_modtype id binders_ast (Enforce mty_ast) [] in Dumpglob.dump_moddef loc mp "mod"; @@ -493,6 +494,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = else (idl,ty)) binders_ast in let mp = Declaremods.declare_module Modintern.interp_modtype Modintern.interp_modexpr + Modintern.interp_modexpr_or_modtype id binders_ast mty_ast_o mexpr_ast_l in Dumpglob.dump_moddef loc mp "mod"; @@ -540,6 +542,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = "and \"Import\" keywords from every functor argument.") else (idl,ty)) binders_ast in let mp = Declaremods.declare_modtype Modintern.interp_modtype + Modintern.interp_modexpr_or_modtype id binders_ast mty_sign mty_ast_l in Dumpglob.dump_moddef loc mp "modtype"; if_verbose message @@ -550,13 +553,8 @@ let vernac_end_modtype (loc,id) = Dumpglob.dump_modref loc mp "modtype"; if_verbose message ("Module Type "^ string_of_id id ^" is defined") -let vernac_include = function - | CIMTE mtys -> - Declaremods.declare_include - Modintern.interp_modtype mtys false - | CIME mexprs -> - Declaremods.declare_include - Modintern.interp_modexpr mexprs true +let vernac_include l = + Declaremods.declare_include Modintern.interp_modexpr_or_modtype l (**********************) (* Gallina extensions *) diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 2df396e09..d95fdbec9 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -176,7 +176,7 @@ type inductive_expr = type one_inductive_expr = lident * local_binder list * constr_expr option * constructor_expr list -type module_binder = bool option * lident list * module_type_ast +type module_binder = bool option * lident list * module_ast type grammar_tactic_prod_item_expr = | TacTerm of string @@ -264,12 +264,12 @@ type vernac_expr = (* Modules and Module Types *) | VernacDeclareModule of bool option * lident * - module_binder list * module_type_ast + module_binder list * module_ast | VernacDefineModule of bool option * lident * - module_binder list * module_type_ast module_signature * module_ast list + module_binder list * module_ast module_signature * module_ast list | VernacDeclareModuleType of lident * - module_binder list * module_type_ast list * module_type_ast list - | VernacInclude of include_ast + module_binder list * module_ast list * module_ast list + | VernacInclude of module_ast list (* Solving *) |