Imported Upstream version 8.1~gammaupstream/8.1.gamma

10 files changed, 73 insertions, 69 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 81401a8e..e9e54cd3 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: declare.ml 8752 2006-04-27 19:37:33Z herbelin $ *)
+(* $Id: declare.ml 9104 2006-09-01 11:04:44Z notin $ *)
 
 open Pp
 open Util
@@ -150,18 +150,18 @@ let open_constant i ((sp,kn),_) =
 let cache_constant ((sp,kn),(cdt,dhyps,imps,kind)) =
   let id = basename sp in
   let _,dir,_ = repr_kn kn in
-  if Idmap.mem id !vartab then
-    errorlabstrm "cache_constant" (pr_id id ++ str " already exists");
-  if Nametab.exists_cci sp then
-    errorlabstrm "cache_constant" (pr_id id ++ str " already exists");
-  let kn' = Global.add_constant dir id cdt in
-  assert (kn' = constant_of_kn kn);
-  Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
-  add_section_constant kn' (Global.lookup_constant kn').const_hyps;
-  Dischargedhypsmap.set_discharged_hyps sp dhyps;
-  with_implicits imps declare_constant_implicits kn';
-  Notation.declare_ref_arguments_scope (ConstRef kn');
-  csttab := Spmap.add sp kind !csttab
+    if Idmap.mem id !vartab then
+      errorlabstrm "cache_constant" (pr_id id ++ str " already exists");
+    if Nametab.exists_cci sp then
+      errorlabstrm "cache_constant" (pr_id id ++ str " already exists");
+    let kn' = Global.add_constant dir id cdt in
+      assert (kn' = constant_of_kn kn);
+      Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
+      add_section_constant kn' (Global.lookup_constant kn').const_hyps;
+      Dischargedhypsmap.set_discharged_hyps sp dhyps;
+      with_implicits imps declare_constant_implicits kn';
+      Notation.declare_ref_arguments_scope (ConstRef kn');
+      csttab := Spmap.add sp kind !csttab
 
 (*s Registration as global tables and rollback. *)
 
diff --git a/library/global.ml b/library/global.ml
index 863d26b7..ab5d8956 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: global.ml 8723 2006-04-16 15:51:02Z herbelin $ *)
+(* $Id: global.ml 9310 2006-10-28 19:35:09Z herbelin $ *)
 
 open Util
 open Names
@@ -141,10 +141,10 @@ open Libnames
 
 let type_of_reference env = function
   | VarRef id -> Environ.named_type id env 
-  | ConstRef c -> Environ.constant_type env c
+  | ConstRef c -> Typeops.type_of_constant env c
   | IndRef ind ->
      let specif = Inductive.lookup_mind_specif env ind in
-      Inductive.type_of_inductive specif
+      Inductive.type_of_inductive env specif
   | ConstructRef cstr ->
      let specif =
       Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
diff --git a/library/goptions.ml b/library/goptions.ml
index c220544c..4d36e1c5 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: goptions.ml 6304 2004-11-16 15:49:08Z sacerdot $ *)
+(* $Id: goptions.ml 9060 2006-07-27 15:30:35Z notin $ *)
 
 (* This module manages customization parameters at the vernacular level     *)
 
@@ -253,7 +253,7 @@ let declare_option cast uncast
 	       unfreeze_function = write;
 	       init_function = (fun () -> write default);
 	       survive_module = false;
-	       survive_section = true}
+	       survive_section = false}
     in 
     fun v -> add_anonymous_leaf (decl_obj v)
   else write
diff --git a/library/impargs.ml b/library/impargs.ml
index 68fc046c..67848d8f 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: impargs.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
+(* $Id: impargs.ml 9310 2006-10-28 19:35:09Z herbelin $ *)
 
 open Util
 open Names
@@ -259,10 +259,9 @@ let list_of_implicits = function
 
 let constants_table = ref Cmap.empty
 
-let compute_constant_implicits kn =
+let compute_constant_implicits cst =
   let env = Global.env () in
-  let cb = lookup_constant kn env in
-  auto_implicits env (body_of_type cb.const_type)
+  auto_implicits env (Typeops.type_of_constant env cst)
 
 let constant_implicits sp =
   try Cmap.find sp !constants_table with Not_found -> No_impl
@@ -282,12 +281,13 @@ let compute_mib_implicits kn =
   let ar =
     Array.to_list
       (Array.map  (* No need to lift, arities contain no de Bruijn *)
-        (fun mip -> (Name mip.mind_typename, None, type_of_inductive (mib,mip)))
+        (fun mip ->
+	  (Name mip.mind_typename, None, type_of_inductive env (mib,mip)))
         mib.mind_packets) in
   let env_ar = push_rel_context ar env in
   let imps_one_inductive i mip =
     let ind = (kn,i) in
-    let ar = type_of_inductive (mib,mip) in
+    let ar = type_of_inductive env (mib,mip) in
     ((IndRef ind,auto_implicits env ar),
      Array.mapi (fun j c -> (ConstructRef (ind,j+1),auto_implicits env_ar c))
        mip.mind_nf_lc)
diff --git a/library/lib.ml b/library/lib.ml
index ba6b9c79..09200a5c 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: lib.ml 8852 2006-05-23 17:52:43Z notin $ *)
+(* $Id: lib.ml 9133 2006-09-12 14:52:07Z notin $ *)
 
 open Pp
 open Util
@@ -186,9 +186,9 @@ let add_leaf id obj =
   if fst (current_prefix ()) = initial_path then 
     error ("No session module started (use -top dir)");
   let oname = make_oname id in
-  cache_object (oname,obj);
-  add_entry oname (Leaf obj);
-  oname
+    cache_object (oname,obj);
+    add_entry oname (Leaf obj);
+    oname
 
 let add_leaves id objs =
   let oname = make_oname id in
@@ -319,7 +319,7 @@ let end_compilation dir =
       | _, OpenedModtype _ -> error "There are some open module types"
       | _ -> assert false
     with
-	Not_found -> ()
+	Not_found -> () 
   in
   let module_p =
     function (_,CompilingLibrary _) -> true | x -> is_something_opened x
@@ -331,16 +331,17 @@ let end_compilation dir =
     with
 	Not_found -> anomaly "No module declared"
   in
-  let _ =  match !comp_name with
+  let _ =  
+    match !comp_name with
       | None -> anomaly "There should be a module name..."
       | Some m ->
 	  if m <> dir then anomaly 
 	    ("The current open module has name "^ (string_of_dirpath m) ^ 
-	     " and not " ^ (string_of_dirpath m));
+	       " and not " ^ (string_of_dirpath m));
   in
   let (after,_,before) = split_lib oname in
-  comp_name := None;
-  !path_prefix,after
+    comp_name := None;
+    !path_prefix,after
 
 (* Returns true if we are inside an opened module type *)
 let is_modtype () = 
@@ -444,15 +445,15 @@ let open_section id =
   let dir = extend_dirpath olddir id in
   let prefix = dir, (mp, extend_dirpath oldsec id) in
   let name = make_path id, make_kn id (* this makes little sense however *) in
-  if Nametab.exists_section dir then
-    errorlabstrm "open_section" (pr_id id ++ str " already exists");
-  let sum = freeze_summaries() in
-  add_entry name (OpenedSection (prefix, sum));
-  (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
-  Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
-  path_prefix := prefix;
-  if !Options.xml_export then !xml_open_section id;
-  add_section ()
+    if Nametab.exists_section dir then
+      errorlabstrm "open_section" (pr_id id ++ str " already exists");
+    let sum = freeze_summaries() in
+      add_entry name (OpenedSection (prefix, sum));
+      (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
+      Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
+      path_prefix := prefix;
+      if !Options.xml_export then !xml_open_section id;
+      add_section ()
 
 
 (* Restore lib_stk and summaries as before the section opening, and
@@ -476,16 +477,16 @@ let close_section id =
       error "no opened section"
   in
   let (secdecls,_,before) = split_lib oname in
-  lib_stk := before;
-  let full_olddir = fst !path_prefix in
-  pop_path_prefix ();
-  add_entry (make_oname id) ClosedSection;
-  if !Options.xml_export then !xml_close_section id;
-  let newdecls = List.map discharge_item secdecls in
-  Summary.section_unfreeze_summaries fs;
-  List.iter (option_iter (fun (id,o) -> ignore (add_leaf id o))) newdecls;
-  Cooking.clear_cooking_sharing ();
-  Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir)
+    lib_stk := before;
+    let full_olddir = fst !path_prefix in
+      pop_path_prefix ();
+      add_entry (make_oname id) ClosedSection;
+      if !Options.xml_export then !xml_close_section id;
+      let newdecls = List.map discharge_item secdecls in
+	Summary.section_unfreeze_summaries fs;
+	List.iter (option_iter (fun (id,o) -> ignore (add_leaf id o))) newdecls;
+	Cooking.clear_cooking_sharing ();
+	Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir)
 
 (*****************)
 (* Backtracking. *)
diff --git a/library/libobject.ml b/library/libobject.ml
index 7f383a3b..709fb1bb 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: libobject.ml 8752 2006-04-27 19:37:33Z herbelin $ *)
+(* $Id: libobject.ml 9104 2006-09-01 11:04:44Z notin $ *)
 
 open Util
 open Names
@@ -144,7 +144,7 @@ let apply_dyn_fun deflt f lobj =
 	  else
 	    anomaly
 	      ("Cannot find library functions for an object with tag "^tag) in 
-  	f dodecl
+	f dodecl
     with
 	Failure "local to_apply_dyn_fun" -> deflt;;
 
diff --git a/library/library.ml b/library/library.ml
index cfd88ca0..43eeb695 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: library.ml 8877 2006-05-30 16:37:04Z notin $ *)
+(* $Id: library.ml 9352 2006-11-07 16:12:10Z notin $ *)
 
 open Pp
 open Util
@@ -300,7 +300,7 @@ let (in_import, out_import) =
 
 (*s Loading from disk to cache (preparation phase) *)
 
-let vo_magic_number = 08003 (* V8.0 final new syntax + new params in ind *)
+let vo_magic_number = 080999 (* V8.1gamma *)
 
 let (raw_extern_library, raw_intern_library) =
   System.raw_extern_intern vo_magic_number ".vo"
@@ -606,7 +606,7 @@ let save_library_to dir f =
     let di = Digest.file f' in
     System.marshal_out ch di;
     close_out ch
-  with e -> (warning ("Removed file "^f');close_out ch; Sys.remove f'; raise e)
+  with e -> (warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise e)
 
 (************************************************************************)
 (*s Display the memory use of a library. *)
diff --git a/library/nameops.ml b/library/nameops.ml
index 1c6a7d56..779f3389 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: nameops.ml 8727 2006-04-24 09:48:06Z herbelin $ *)
+(* $Id: nameops.ml 9225 2006-10-09 15:59:23Z herbelin $ *)
 
 open Pp
 open Util
@@ -154,6 +154,10 @@ let name_app f = function
   | Name id -> Name (f id)
   | Anonymous -> Anonymous
 
+let name_fold_map f e = function
+  | Name id -> let (e,id) = f e id in (e,Name id)
+  | Anonymous -> e,Anonymous
+
 let next_name_away_with_default default name l = 
   match name with
     | Name str  -> next_ident_away str l
diff --git a/library/nameops.mli b/library/nameops.mli
index 9d1722d4..8e291761 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: nameops.mli 6616 2005-01-21 17:18:23Z herbelin $ i*)
+(*i $Id: nameops.mli 9225 2006-10-09 15:59:23Z herbelin $ i*)
 
 open Names
 
@@ -38,6 +38,8 @@ val out_name : name -> identifier
 val name_fold : (identifier -> 'a -> 'a) -> name -> 'a -> 'a
 val name_cons : name -> identifier list -> identifier list
 val name_app : (identifier -> identifier) -> name -> name
+val name_fold_map : ('a -> identifier -> 'a * identifier) -> 'a -> name -> 'a * name
+
 
 val pr_lab : label -> Pp.std_ppcmds
 
diff --git a/library/states.ml b/library/states.ml
index 3bb37a4d..169a3857 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -6,16 +6,16 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: states.ml 6692 2005-02-06 13:03:51Z herbelin $ *)
+(* $Id: states.ml 9100 2006-08-31 18:04:26Z herbelin $ *)
 
 open System
 
 type state = Lib.frozen * Summary.frozen
 
-let get_state () =
+let freeze () =
   (Lib.freeze(), Summary.freeze_summaries())
 
-let set_state (fl,fs) =
+let unfreeze (fl,fs) =
   Lib.unfreeze fl;
   Summary.unfreeze_summaries fs
 
@@ -23,17 +23,14 @@ let state_magic_number = 19764
 
 let (extern_state,intern_state) =
   let (raw_extern, raw_intern) = extern_intern state_magic_number ".coq" in
-  (fun s -> raw_extern s (get_state())),
-  (fun s -> set_state (raw_intern (Library.get_load_paths ()) s))
+  (fun s -> raw_extern s (freeze())),
+  (fun s -> unfreeze (raw_intern (Library.get_load_paths ()) s))
 
 (* Rollback. *)
 
-let freeze = get_state
-let unfreeze = set_state
-
 let with_heavy_rollback f x =
-  let st = get_state () in
+  let st = freeze () in
   try 
     f x
   with reraise ->
-    (set_state st; raise reraise)
+    (unfreeze st; raise reraise)