diff options
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 |