diff options
| author | barras | 2001-11-12 12:38:08 +0000 |
|---|---|---|
| committer | barras | 2001-11-12 12:38:08 +0000 |
| commit | 865d3a274dc618a4eff13b309109aa559077a933 (patch) | |
| tree | dac5bc457e5ad9b955b21012b230ed97de22d92b /library | |
| parent | da33e695040678d74622213af2cd43d32140d186 (diff) | |
Suites modifs du noyau. Univ devient purement fonctionnel.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 2 | ||||
| -rw-r--r-- | library/impargs.mli | 1 | ||||
| -rw-r--r-- | library/lib.ml | 1 |
3 files changed, 1 insertions, 3 deletions
diff --git a/library/declare.ml b/library/declare.ml index 9fa7b14771..816a456154 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -377,7 +377,7 @@ let last_section_hyps dir = if dir=p then id::sec_ids else sec_ids with Not_found -> sec_ids) (Environ.named_context (Global.env())) - [] + ~init:[] let constr_of_reference = function | VarRef id -> mkVar id diff --git a/library/impargs.mli b/library/impargs.mli index 46d03d996d..470f3d0c35 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -12,7 +12,6 @@ open Names open Term open Environ -open Inductive open Nametab (*i*) diff --git a/library/lib.ml b/library/lib.ml index 17b8fa8da0..b2e73d1ce0 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -129,7 +129,6 @@ let start_module s = if !path_prefix <> default_module then error "some sections are already opened"; module_name := Some s; - Univ.set_module s; let _ = add_anonymous_entry (Module s) in path_prefix := s |