diff options
| -rw-r--r-- | kernel/safe_typing.ml | 43 | ||||
| -rw-r--r-- | library/declaremods.ml | 1 | ||||
| -rw-r--r-- | library/library.ml | 22 | ||||
| -rw-r--r-- | theories/FSets/FSetDecide.v | 6 | ||||
| -rw-r--r-- | theories/MSets/MSetDecide.v | 6 | ||||
| -rw-r--r-- | theories/Program/Wf.v | 3 |
6 files changed, 18 insertions, 63 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index bd44b3967..5f8d8b977 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -85,9 +85,6 @@ open Declarations - [type_in_type] : does the universe hierarchy collapse? - [imports] : names and digests of Require'd libraries since big-bang. This field will only grow - - [loads] : list of libraries Require'd inside the current module. - They will be propagated to the upper module level when - the current module ends. - [local_retroknowledge] *) @@ -124,7 +121,6 @@ type safe_environment = engagement : engagement option; type_in_type : bool; imports : vodigest DPMap.t; - loads : (module_path * module_body) list; local_retroknowledge : Retroknowledge.action list } and modvariant = @@ -153,7 +149,6 @@ let empty_environment = engagement = None; type_in_type = false; imports = DPMap.empty; - loads = []; local_retroknowledge = [] } let is_initial senv = @@ -289,8 +284,7 @@ let check_empty_context senv = it must have been freshly started *) let check_empty_struct senv = - assert (List.is_empty senv.revstruct - && List.is_empty senv.loads) + assert (List.is_empty senv.revstruct) (** When starting a library, the current environment should be initial i.e. only composed of Require's *) @@ -565,12 +559,6 @@ let add_module_parameter mbid mte inl senv = let functorize params init = List.fold_left (fun e (mbid,mt) -> MoreFunctor(mbid,mt,e)) init params -let propagate_loads senv = - List.fold_left - (fun env (_,mb) -> full_add_module mb env) - senv - (List.rev senv.loads) - (** Build the module body of the current module, taking in account a possible return type (_:T) *) @@ -615,7 +603,6 @@ let propagate_senv newdef newenv newresolver senv oldsenv = (* engagement is propagated to the upper level *) engagement = senv.engagement; imports = senv.imports; - loads = senv.loads@oldsenv.loads; local_retroknowledge = senv.local_retroknowledge@oldsenv.local_retroknowledge } @@ -629,7 +616,7 @@ let end_module l restype senv = let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in let newenv = set_engagement_opt newenv senv.engagement in let senv'= - propagate_loads { senv with + { senv with env = newenv; univ = Univ.Constraint.union senv.univ mb.mod_constraints} in let newenv = Environ.add_constraints mb.mod_constraints senv'.env in @@ -651,7 +638,7 @@ let end_modtype l senv = let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in let newenv = Environ.add_constraints senv.univ newenv in let newenv = set_engagement_opt newenv senv.engagement in - let senv' = propagate_loads {senv with env=newenv} in + let senv' = {senv with env=newenv} in let mtb = { typ_mp = mp; typ_expr = functorize params auto_tb; @@ -799,8 +786,7 @@ let import lib cst vodigest senv = in Modops.add_linked_module mb linkinfo env); modresolver = Mod_subst.add_delta_resolver mb.mod_delta senv.modresolver; - imports = DPMap.add lib.comp_name vodigest senv.imports; - loads = (mp,mb)::senv.loads } + imports = DPMap.add lib.comp_name vodigest senv.imports } (** {6 Safe typing } *) @@ -844,27 +830,6 @@ let register_inline kn senv = let add_constraints c = add_constraints (Now c) - -(* NB: The next old comment probably refers to [propagate_loads] above. - When a Require is done inside a module, we'll redo this require - at the upper level after the module is ended, and so on. - This is probably not a big deal anyway, since these Require's - inside modules should be pretty rare. Maybe someday we could - brutally forbid this tricky "feature"... *) - -(* we have an inefficiency: Since loaded files are added to the -environment every time a module is closed, their components are -calculated many times. This could be avoided in several ways: - -1 - for each file create a dummy environment containing only this -file's components, merge this environment with the global -environment, and store for the future (instead of just its type) - -2 - create "persistent modules" environment table in Environ add put -loaded by side-effect once and for all (like it is done in OCaml). -Would this be correct with respect to undo's and stuff ? -*) - let set_strategy e k l = { e with env = (Environ.set_oracle e.env (Conv_oracle.set_strategy (Environ.oracle e.env) k l)) } diff --git a/library/declaremods.ml b/library/declaremods.ml index 33d37ef62..5c245064f 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -850,6 +850,7 @@ let library_values = Summary.ref (Dirmap.empty : library_values Dirmap.t) ~name:"LIBVALUES" let register_library dir cenv (objs:library_objects) digest univ = + assert (not (Lib.is_module_or_modtype ())); let mp = MPfile dir in let () = try diff --git a/library/library.ml b/library/library.ml index 343588652..20fc31961 100644 --- a/library/library.ml +++ b/library/library.ml @@ -533,18 +533,12 @@ let in_require : require_obj -> obj = if [export = Some true] *) let require_library_from_dirpath modrefl export = + if Lib.is_module_or_modtype () then + error "Require is not allowed inside a module or a module type"; let needed, contents = List.fold_left rec_intern_library ([], DPMap.empty) modrefl in let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in let modrefl = List.map fst modrefl in - if Lib.is_module_or_modtype () then - begin - add_anonymous_leaf (in_require (needed,modrefl,None)); - Option.iter (fun exp -> - List.iter (fun dir -> add_anonymous_leaf (in_import(dir,exp))) modrefl) - export - end - else - add_anonymous_leaf (in_require (needed,modrefl,export)); + add_anonymous_leaf (in_require (needed,modrefl,export)); add_frozen_state () let require_library qidl export = @@ -552,15 +546,11 @@ let require_library qidl export = require_library_from_dirpath modrefl export let require_library_from_file idopt file export = + if Lib.is_module_or_modtype () then + error "Require is not allowed inside a module or a module type"; let modref,needed = rec_intern_library_from_file idopt file in let needed = List.rev_map snd needed in - if Lib.is_module_or_modtype () then begin - add_anonymous_leaf (in_require (needed,[modref],None)); - Option.iter (fun exp -> add_anonymous_leaf (in_import (modref,exp))) - export - end - else - add_anonymous_leaf (in_require (needed,[modref],export)); + add_anonymous_leaf (in_require (needed,[modref],export)); add_frozen_state () (* the function called by Vernacentries.vernac_import *) diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v index f64df9fe1..ad067eb3d 100644 --- a/theories/FSets/FSetDecide.v +++ b/theories/FSets/FSetDecide.v @@ -15,7 +15,7 @@ (** This file implements a decision procedure for a certain class of propositions involving finite sets. *) -Require Import Decidable DecidableTypeEx FSetFacts. +Require Import Decidable Setoid DecidableTypeEx FSetFacts. (** First, a version for Weak Sets in functorial presentation *) @@ -115,8 +115,8 @@ the above form: not affect the namespace if you import the enclosing module [Decide]. *) Module FSetLogicalFacts. - Require Export Decidable. - Require Export Setoid. + Export Decidable. + Export Setoid. (** ** Lemmas and Tactics About Decidable Propositions *) diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v index eefd2951f..f2555791b 100644 --- a/theories/MSets/MSetDecide.v +++ b/theories/MSets/MSetDecide.v @@ -15,7 +15,7 @@ (** This file implements a decision procedure for a certain class of propositions involving finite sets. *) -Require Import Decidable DecidableTypeEx MSetFacts. +Require Import Decidable Setoid DecidableTypeEx MSetFacts. (** First, a version for Weak Sets in functorial presentation *) @@ -115,8 +115,8 @@ the above form: not affect the namespace if you import the enclosing module [Decide]. *) Module MSetLogicalFacts. - Require Export Decidable. - Require Export Setoid. + Export Decidable. + Export Setoid. (** ** Lemmas and Tactics About Decidable Propositions *) diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index c483b1d83..25ea6b726 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -11,6 +11,7 @@ Require Import Coq.Init.Wf. Require Import Coq.Program.Utils. Require Import ProofIrrelevance. +Require Import FunctionalExtensionality. Local Open Scope program_scope. @@ -221,8 +222,6 @@ Ltac fold_sub f := Module WfExtensionality. - Require Import FunctionalExtensionality. - (** The two following lemmas allow to unfold a well-founded fixpoint definition without restriction using the functional extensionality axiom. *) |