Merge remote-tracking branch 'origin/master' into stm+doc_hook

12 files changed, 42 insertions, 132 deletions

diff --git a/library/global.ml b/library/global.ml
index d9f8a6ffa3..58e2380440 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -94,7 +94,8 @@ let make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative
 let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b)
 let sprop_allowed () = Environ.sprop_allowed (env())
 let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd)
-let add_constant ~in_section id d = globalize (Safe_typing.add_constant ~in_section (i2l id) d)
+let add_constant ?role ~in_section id d = globalize (Safe_typing.add_constant ?role ~in_section (i2l id) d)
+let add_recipe ~in_section id d = globalize (Safe_typing.add_recipe ~in_section (i2l id) d)
 let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie)
 let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
 let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl)
@@ -157,12 +158,6 @@ let import c u d = globalize (Safe_typing.import c u d)
 let env_of_context hyps =
   reset_with_named_context hyps (env())
 
-let constr_of_global_in_context = Typeops.constr_of_global_in_context
-let type_of_global_in_context = Typeops.type_of_global_in_context
-
-let universes_of_global gr = 
-  universes_of_global (env ()) gr
-
 let is_polymorphic r = Environ.is_polymorphic (env()) r
 
 let is_template_polymorphic r = is_template_polymorphic (env ()) r
diff --git a/library/global.mli b/library/global.mli
index ca88d2dafd..984d8c666c 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -46,7 +46,8 @@ val export_private_constants : in_section:bool ->
   unit Entries.definition_entry * Safe_typing.exported_private_constant list
 
 val add_constant :
-  in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t
+  ?role:Entries.side_effect_role -> in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t * Safe_typing.private_constants
+val add_recipe : in_section:bool -> Id.t -> Cooking.recipe -> Constant.t
 val add_mind :
   Id.t -> Entries.mutual_inductive_entry -> MutInd.t
 
@@ -84,7 +85,7 @@ val add_module_parameter :
 (** {6 Queries in the global environment } *)
 
 val lookup_named     : variable -> Constr.named_declaration
-val lookup_constant  : Constant.t -> Declarations.constant_body
+val lookup_constant  : Constant.t -> Opaqueproof.opaque Declarations.constant_body
 val lookup_inductive : inductive ->
   Declarations.mutual_inductive_body * Declarations.one_inductive_body
 val lookup_pinductive : Constr.pinductive -> 
@@ -105,7 +106,7 @@ val body_of_constant : Constant.t -> (Constr.constr * Univ.AUContext.t) option
     polymorphic constants, the term contains De Bruijn universe variables that
     need to be instantiated. *)
 
-val body_of_constant_body : Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option
+val body_of_constant_body : Opaqueproof.opaque Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option
 (** Same as {!body_of_constant} but on {!Declarations.constant_body}. *)
 
 (** {6 Compiled libraries } *)
@@ -131,18 +132,6 @@ val is_polymorphic : GlobRef.t -> bool
 val is_template_polymorphic : GlobRef.t -> bool
 val is_type_in_type : GlobRef.t -> bool
 
-val constr_of_global_in_context : Environ.env ->
-  GlobRef.t -> Constr.types * Univ.AUContext.t
-  [@@ocaml.deprecated "alias of [Typeops.constr_of_global_in_context]"]
-
-val type_of_global_in_context : Environ.env -> 
-  GlobRef.t -> Constr.types * Univ.AUContext.t
-  [@@ocaml.deprecated "alias of [Typeops.type_of_global_in_context]"]
-
-(** Returns the universe context of the global reference (whatever its polymorphic status is). *)
-val universes_of_global : GlobRef.t -> Univ.AUContext.t
-[@@ocaml.deprecated "Use [Environ.universes_of_global]"]
-
 (** {6 Retroknowledge } *)
 
 val register_inline : Constant.t -> unit
diff --git a/library/globnames.ml b/library/globnames.ml
index db2e8bfaed..99dcc43ad1 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -85,15 +85,6 @@ let printable_constr_of_global = function
   | ConstructRef sp -> mkConstruct sp
   | IndRef sp -> mkInd sp
 
-module RefOrdered = Names.GlobRef.Ordered
-module RefOrdered_env = Names.GlobRef.Ordered_env
-
-module Refmap = Names.GlobRef.Map
-module Refset = Names.GlobRef.Set
-
-module Refmap_env = Names.GlobRef.Map_env
-module Refset_env = Names.GlobRef.Set_env
-
 (* Extended global references *)
 
 type syndef_name = KerName.t
@@ -134,6 +125,3 @@ end
 type global_reference_or_constr = 
   | IsGlobal of global_reference
   | IsConstr of constr
-
-(* Deprecated *)
-let eq_gr = GlobRef.equal
diff --git a/library/globnames.mli b/library/globnames.mli
index d49ed453f5..14e422b743 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -25,8 +25,6 @@ val isConstRef : GlobRef.t -> bool
 val isIndRef : GlobRef.t -> bool
 val isConstructRef : GlobRef.t -> bool
 
-val eq_gr : GlobRef.t -> GlobRef.t -> bool
-[@@ocaml.deprecated "Use Names.GlobRef.equal"]
 val canonical_gr : GlobRef.t -> GlobRef.t
 
 val destVarRef : GlobRef.t -> variable
@@ -48,22 +46,6 @@ val printable_constr_of_global : GlobRef.t -> constr
    raise [Not_found] if not a global reference *)
 val global_of_constr : constr -> GlobRef.t
 
-module RefOrdered = Names.GlobRef.Ordered
-[@@ocaml.deprecated "Use Names.GlobRef.Ordered"]
-
-module RefOrdered_env = Names.GlobRef.Ordered_env
-[@@ocaml.deprecated "Use Names.GlobRef.Ordered_env"]
-
-module Refset = Names.GlobRef.Set
-[@@ocaml.deprecated "Use Names.GlobRef.Set"]
-module Refmap = Names.GlobRef.Map
-[@@ocaml.deprecated "Use Names.GlobRef.Map"]
-
-module Refset_env = GlobRef.Set_env
-[@@ocaml.deprecated "Use Names.GlobRef.Set_env"]
-module Refmap_env = GlobRef.Map_env
-[@@ocaml.deprecated "Use Names.GlobRef.Map_env"]
-
 (** {6 Extended global references } *)
 
 type syndef_name = KerName.t
diff --git a/library/goptions.ml b/library/goptions.ml
index b9c1802a72..f4b8ce9465 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -42,13 +42,12 @@ let error_undeclared_key key =
 (****************************************************************************)
 (* 1- Tables                                                                *)
 
-class type ['a] table_of_A =
-object
-  method add : 'a -> unit
-  method remove : 'a -> unit
-  method mem : 'a -> unit
-  method print : unit
-end
+type 'a table_of_A =  {
+  add : Environ.env -> 'a -> unit;
+  remove : Environ.env -> 'a -> unit;
+  mem : Environ.env -> 'a -> unit;
+  print : unit -> unit;
+}
 
 module MakeTable =
   functor
@@ -109,18 +108,17 @@ module MakeTable =
 		 (fun a b -> spc () ++ printer a ++ b)
 		 table (mt ()) ++ str "." ++ fnl ())))
 
-    class table_of_A () =
-    object
-      method add x = add_option (A.encode (Global.env()) x)
-      method remove x = remove_option (A.encode (Global.env()) x)
-      method mem x =
-        let y = A.encode (Global.env()) x in
+    let table_of_A = {
+       add = (fun env x -> add_option (A.encode env x));
+       remove = (fun env x -> remove_option (A.encode env x));
+       mem = (fun env x ->
+        let y = A.encode env x in
         let answer = MySet.mem y !t in
-        Feedback.msg_info (A.member_message y answer)
-      method print = print_table A.title A.printer !t
-    end
+        Feedback.msg_info (A.member_message y answer));
+       print = (fun () -> print_table A.title A.printer !t);
+     }
 
-    let _ = A.table := (nick,new table_of_A ())::!A.table
+    let _ = A.table := (nick, table_of_A)::!A.table
     let active c = MySet.mem c !t
     let elements () = MySet.elements !t
   end
diff --git a/library/goptions.mli b/library/goptions.mli
index 2e593e9d9e..381ba4d34a 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -76,7 +76,7 @@ end
 
 (** The functor [MakeRefTable] declares a new table of objects of type
    [A.t] practically denoted by [reference]; the encoding function
-   [encode : reference -> A.t] is typically a globalization function,
+   [encode : env -> reference -> A.t] is typically a globalization function,
    possibly with some restriction checks; the function
    [member_message] say what to print when invoking the "Test Toto
    Titi foo." command; at the end [title] is the table name printed
@@ -139,19 +139,17 @@ val declare_bool_option_and_ref : depr:bool -> name:string -> key:option_name ->
 
 module OptionMap : CSig.MapS with type key = option_name
 
-val get_string_table :
-  option_name ->
-    < add : string -> unit;
-      remove : string -> unit;
-      mem : string -> unit;
-      print : unit >
+type 'a table_of_A =  {
+  add : Environ.env -> 'a -> unit;
+  remove : Environ.env -> 'a -> unit;
+  mem : Environ.env -> 'a -> unit;
+  print : unit -> unit;
+}
 
+val get_string_table :
+  option_name -> string table_of_A
 val get_ref_table :
-  option_name ->
-    < add : qualid -> unit;
-      remove : qualid -> unit;
-      mem : qualid -> unit;
-      print : unit >
+  option_name -> qualid table_of_A
 
 (** The first argument is a locality flag. *)
 val set_int_option_value_gen    : ?locality:option_locality -> option_name -> int option -> unit
diff --git a/library/lib.ml b/library/lib.ml
index d4381a6923..4be288ed20 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -211,9 +211,6 @@ let split_lib_at_opening sp =
 let add_entry sp node =
   lib_state := { !lib_state with lib_stk = (sp,node) :: !lib_state.lib_stk }
 
-let pull_to_head oname =
-  lib_state := { !lib_state with lib_stk = (oname,List.assoc oname !lib_state.lib_stk) :: List.remove_assoc oname !lib_state.lib_stk }
-
 let anonymous_id =
   let n = ref 0 in
   fun () -> incr n; Names.Id.of_string ("_" ^ (string_of_int !n))
@@ -278,7 +275,7 @@ let start_mod is_type export id mp fs =
   let prefix = Nametab.{ obj_dir = dir; obj_mp = mp; obj_sec = Names.DirPath.empty } in
   let exists =
     if is_type then Nametab.exists_cci (make_path id)
-    else Nametab.exists_module dir
+    else Nametab.exists_dir dir
   in
   if exists then
     user_err ~hdr:"open_module" (Id.print id ++ str " already exists");
@@ -569,7 +566,7 @@ let open_section id =
   let opp = !lib_state.path_prefix in
   let obj_dir = add_dirpath_suffix opp.Nametab.obj_dir id in
   let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in
-  if Nametab.exists_section obj_dir then
+  if Nametab.exists_dir obj_dir then
     user_err ~hdr:"open_section" (Id.print id ++ str " already exists.");
   let fs = Summary.freeze_summaries ~marshallable:false in
   add_entry (make_foname id) (OpenedSection (prefix, fs));
diff --git a/library/lib.mli b/library/lib.mli
index 30569197bc..5da76961a6 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -57,7 +57,6 @@ val segment_of_objects :
 
 val add_leaf : Id.t -> Libobject.obj -> Libobject.object_name
 val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit
-val pull_to_head : Libobject.object_name -> unit
 
 (** this operation adds all objects with the same name and calls [load_object]
    for each of them *)
diff --git a/library/library.ml b/library/library.ml
index 04e38296d9..500e77f89b 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -612,8 +612,6 @@ let import_module export modl =
 (*s Initializing the compilation of a library. *)
 
 let load_library_todo f =
-  let longf = Loadpath.locate_file (f^".v") in
-  let f = longf^"io" in
   let ch = raw_intern_library f in
   let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in
   let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in
@@ -626,7 +624,7 @@ let load_library_todo f =
   if s2 = None then user_err ~hdr:"restart" (str"not a .vio file");
   if s3 = None then user_err ~hdr:"restart" (str"not a .vio file");
   if pi3 (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file");
-  longf, s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5
+  s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5
 
 (************************************************************************)
 (*s [save_library dir] ends library [dir] and save it to the disk. *)
@@ -727,14 +725,13 @@ let save_library_to ?todo ~output_native_objects dir f otab =
     iraise reraise
 
 let save_library_raw f sum lib univs proofs =
-  let f' = f^"o" in
-  let ch = raw_extern_library f' in
-  System.marshal_out_segment f' ch (sum        : seg_sum);
-  System.marshal_out_segment f' ch (lib        : seg_lib);
-  System.marshal_out_segment f' ch (Some univs : seg_univ option);
-  System.marshal_out_segment f' ch (None       : seg_discharge option);
-  System.marshal_out_segment f' ch (None       : 'tasks option);
-  System.marshal_out_segment f' ch (proofs     : seg_proofs);
+  let ch = raw_extern_library f in
+  System.marshal_out_segment f ch (sum        : seg_sum);
+  System.marshal_out_segment f ch (lib        : seg_lib);
+  System.marshal_out_segment f ch (Some univs : seg_univ option);
+  System.marshal_out_segment f ch (None       : seg_discharge option);
+  System.marshal_out_segment f ch (None       : 'tasks option);
+  System.marshal_out_segment f ch (proofs     : seg_proofs);
   close_out ch
 
 module StringOrd = struct type t = string let compare = String.compare end
diff --git a/library/library.mli b/library/library.mli
index a976be0184..390299bf56 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -46,7 +46,7 @@ val save_library_to :
   DirPath.t -> string -> Opaqueproof.opaquetab -> unit
 
 val load_library_todo :
-  string -> string * seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs
+  string -> seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs
 val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit
 
 (** {6 Interrogate the status of libraries } *)
diff --git a/library/nametab.ml b/library/nametab.ml
index 95890b2edf..bd0ea5f04f 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -43,12 +43,6 @@ module GlobDirRef = struct
 
 end
 
-type global_dir_reference = GlobDirRef.t
-[@@ocaml.deprecated "Use [GlobDirRef.t]"]
-
-let eq_global_dir_reference = GlobDirRef.equal
-[@@ocaml.deprecated "Use [GlobDirRef.equal]"]
-
 exception GlobalizationError of qualid
 
 let error_global_not_found qid =
@@ -516,10 +510,6 @@ let exists_cci sp = ExtRefTab.exists sp !the_ccitab
 
 let exists_dir dir = DirTab.exists dir !the_dirtab
 
-let exists_section = exists_dir
-
-let exists_module = exists_dir
-
 let exists_modtype sp = MPTab.exists sp !the_modtypetab
 
 let exists_universe kn = UnivTab.exists kn !the_univtab
@@ -585,10 +575,3 @@ let global_inductive qid =
   | ref ->
       user_err ?loc:qid.CAst.loc ~hdr:"global_inductive"
         (pr_qualid qid ++ spc () ++ str "is not an inductive type")
-
-(********************************************************************)
-
-(* Deprecated synonyms *)
-
-let extended_locate = locate_extended
-let absolute_reference = global_of_path
diff --git a/library/nametab.mli b/library/nametab.mli
index fccb8fd918..a4f177aad0 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -89,13 +89,6 @@ module GlobDirRef : sig
   val equal : t -> t -> bool
 end
 
-type global_dir_reference = GlobDirRef.t
-[@@ocaml.deprecated "Use [GlobDirRef.t]"]
-
-val eq_global_dir_reference :
-  GlobDirRef.t -> GlobDirRef.t -> bool
-[@@ocaml.deprecated "Use [GlobDirRef.equal]"]
-
 exception GlobalizationError of qualid
 
 (** Raises a globalization error *)
@@ -170,10 +163,6 @@ val extended_global_of_path : full_path -> extended_global_reference
 val exists_cci : full_path -> bool
 val exists_modtype : full_path -> bool
 val exists_dir : DirPath.t -> bool
-val exists_section : DirPath.t -> bool (** deprecated synonym of [exists_dir] *)
-
-val exists_module : DirPath.t -> bool (** deprecated synonym of [exists_dir] *)
-
 val exists_universe : full_path -> bool
 
 (** {6 These functions locate qualids into full user names } *)
@@ -220,11 +209,6 @@ val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid
 val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid
 val shortest_qualid_of_universe : ?loc:Loc.t -> Univ.Level.UGlobal.t -> qualid
 
-(** Deprecated synonyms *)
-
-val extended_locate : qualid -> extended_global_reference (*= locate_extended *)
-val absolute_reference : full_path -> GlobRef.t (** = global_of_path *)
-
 (** {5 Generic name handling} *)
 
 (** NOT FOR PUBLIC USE YET. Plugin writers, please do not rely on this API. *)