From 865d3a274dc618a4eff13b309109aa559077a933 Mon Sep 17 00:00:00 2001
From: barras
Date: Mon, 12 Nov 2001 12:38:08 +0000
Subject: 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
---
 library/declare.ml  | 2 +-
 library/impargs.mli | 1 -
 library/lib.ml      | 1 -
 3 files changed, 1 insertion(+), 3 deletions(-)

(limited to 'library')

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
 
-- 
cgit v1.2.3