From 3d09e39dd423d81c6af3e991d5b282ea8608646b Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 17 Jul 2013 15:31:36 +0000 Subject: More dynamic argument scopes When arguments scopes are set manually, nothing new, they stay as they are (until maybe another Arguments invocation). But when argument scopes are computed out of the argument type and the Bind Scope information, this kind of scope is now dynamic: a later Bind Scope will be able to impact the scopes of an earlier constant. For Instance: Definition f (n:nat) := n. About f. (* Argument scope is [nat_scope] *) Bind Scope other_scope with nat. About f. (* Argument scope is [other_scope] *) This allows to get rid of hacks for modifying scopes during functor applications. Moreover, the subst_arguments_scope is now environment-insensitive (needed for forthcoming changes in declaremods). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16626 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/declaremods.mli | 27 +++++++++++---------------- 1 file changed, 11 insertions(+), 16 deletions(-) (limited to 'library/declaremods.mli') diff --git a/library/declaremods.mli b/library/declaremods.mli index 06a4edd84..b76017286 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -16,11 +16,6 @@ open Libobject open Lib open Vernacexpr -(** This modules provides official functions to declare modules and - module types *) - -val subst_scope : string -> string - (** {6 Modules } *) (** [declare_module interp_modtype interp_modexpr id fargs typ expr] @@ -40,14 +35,14 @@ val declare_module : (env -> 'modast -> module_struct_entry) -> (env -> 'modast -> module_struct_entry * bool) -> Id.t -> - (Id.t located list * ('modast annotated)) list -> - ('modast annotated) module_signature -> - ('modast annotated) list -> module_path + (Id.t located list * ('modast * inline)) list -> + ('modast * inline) module_signature -> + ('modast * inline) list -> module_path val start_module : (env -> 'modast -> module_struct_entry) -> bool option -> Id.t -> - (Id.t located list * ('modast annotated)) list -> - ('modast annotated) module_signature -> module_path + (Id.t located list * ('modast * inline)) list -> + ('modast * inline) module_signature -> module_path val end_module : unit -> module_path @@ -58,14 +53,14 @@ val end_module : unit -> module_path val declare_modtype : (env -> 'modast -> module_struct_entry) -> (env -> 'modast -> module_struct_entry * bool) -> Id.t -> - (Id.t located list * ('modast annotated)) list -> - ('modast annotated) list -> - ('modast annotated) list -> + (Id.t located list * ('modast * inline)) list -> + ('modast * inline) list -> + ('modast * inline) list -> module_path val start_modtype : (env -> 'modast -> module_struct_entry) -> - Id.t -> (Id.t located list * ('modast annotated)) list -> - ('modast annotated) list -> module_path + Id.t -> (Id.t located list * ('modast * inline)) list -> + ('modast * inline) list -> module_path val end_modtype : unit -> module_path @@ -110,7 +105,7 @@ val import_module : bool -> module_path -> unit (** Include *) val declare_include : (env -> 'struct_expr -> module_struct_entry * bool) -> - ('struct_expr annotated) list -> unit + ('struct_expr * inline) list -> unit (** {6 ... } *) (** [iter_all_segments] iterate over all segments, the modules' -- cgit v1.2.3