From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Fri, 8 Aug 2008 13:18:42 +0200
Subject: Imported Upstream version 8.2~beta4+dfsg

---
 library/declare.ml | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

(limited to 'library/declare.ml')

diff --git a/library/declare.ml b/library/declare.ml
index 07810e3c..4bdc11c3 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: declare.ml 10840 2008-04-23 21:29:34Z herbelin $ *)
+(* $Id: declare.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 (** This module is about the low-level declaration of logical objects *)
 
@@ -57,10 +57,12 @@ let cache_variable ((sp,_),o) =
   let impl,opaq,cst,keep = match d with (* Fails if not well-typed *)
     | SectionLocalAssum (ty, impl, keep) ->
         let cst = Global.push_named_assum (id,ty) in
-        impl, true, cst, (if keep then Some ty else None)
+	let impl = if impl then Lib.Implicit else Lib.Explicit in
+	let keep = if keep then Some ty else None in
+	impl, true, cst, keep
     | SectionLocalDef (c,t,opaq) -> 
         let cst = Global.push_named_def (id,c,t) in
-        false, opaq, cst, None in
+        Lib.Explicit, opaq, cst, None in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
   add_section_variable id impl keep;
   Dischargedhypsmap.set_discharged_hyps sp [];
@@ -116,7 +118,7 @@ let cache_constant ((sp,kn),(cdt,dhyps,kind)) =
 
 let discharged_hyps kn sechyps =
   let (_,dir,_) = repr_kn kn in
-  let args = array_map_to_list destVar (instance_from_named_context sechyps) in
+  let args = Array.to_list (instance_from_variable_context sechyps) in
   List.rev (List.map (Libnames.make_path dir) args)
 
 let discharge_constant ((sp,kn),(cdt,dhyps,kind)) =
@@ -124,7 +126,7 @@ let discharge_constant ((sp,kn),(cdt,dhyps,kind)) =
   let cb = Global.lookup_constant con in
   let repl = replacement_context () in
   let sechyps = section_segment_of_constant con in
-  let recipe = { d_from=cb; d_modlist=repl; d_abstract=sechyps } in
+  let recipe = { d_from=cb; d_modlist=repl; d_abstract=named_of_variable_context sechyps } in
   Some (GlobalRecipe recipe,(discharged_hyps kn sechyps)@dhyps,kind)
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
@@ -235,7 +237,7 @@ let discharge_inductive ((sp,kn),(dhyps,mie)) =
   let repl = replacement_context () in
   let sechyps = section_segment_of_mutual_inductive kn in
   Some (discharged_hyps kn sechyps,
-        Discharge.process_inductive sechyps repl mie)
+        Discharge.process_inductive (named_of_variable_context sechyps) repl mie)
 
 let dummy_one_inductive_entry mie = {
   mind_entry_typename = mie.mind_entry_typename;
-- 
cgit v1.2.3