From 478db417e1a3a493870f012495bbc7348581ac17 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 12 Apr 2019 15:23:57 +0200
Subject: Remove `constr_of_global_in_context`

This function seems unused.
---
 library/global.ml  | 1 -
 library/global.mli | 4 ----
 2 files changed, 5 deletions(-)

(limited to 'library')

diff --git a/library/global.ml b/library/global.ml
index d9f8a6ffa3..55aed1c56e 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -157,7 +157,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 = 
diff --git a/library/global.mli b/library/global.mli
index ca88d2dafd..76ac3f6279 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -131,10 +131,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]"]
-- 
cgit v1.2.3


From 77257819ea4a381067e65fd46e7d7590aa7e2600 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 11 Apr 2019 12:45:07 +0200
Subject: Remove Global.env from goptions by passing from vernacentries

Currently this env is only used to error for Printing If/Let on
non-2-constructor/non-1-constructor types so we could alternatively
remove it and not error / error later when trying to print.
Keeping the env and the error as-is should be fine though.
---
 library/goptions.ml  | 32 +++++++++++++++-----------------
 library/goptions.mli | 22 ++++++++++------------
 2 files changed, 25 insertions(+), 29 deletions(-)

(limited to 'library')

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


From 1cdaa823aa2db2f68cf63561a85771bb98aec70f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 2 Apr 2019 13:22:11 +0200
Subject: [api] Remove 8.10 deprecations.

Some of them are significant so presumably it will take a bit of
effort to fix overlays.

I left out the removal of `nf_enter` for now as MTac2 needs some
serious porting in order to avoid it.
---
 library/global.ml     |  5 -----
 library/global.mli    |  8 --------
 library/globnames.ml  | 12 ------------
 library/globnames.mli | 18 ------------------
 library/lib.ml        |  4 ++--
 library/nametab.ml    | 17 -----------------
 library/nametab.mli   | 16 ----------------
 7 files changed, 2 insertions(+), 78 deletions(-)

(limited to 'library')

diff --git a/library/global.ml b/library/global.ml
index 55aed1c56e..06e06a8cf2 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -157,11 +157,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 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 76ac3f6279..a60de48897 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -131,14 +131,6 @@ val is_polymorphic : GlobRef.t -> bool
 val is_template_polymorphic : GlobRef.t -> bool
 val is_type_in_type : GlobRef.t -> bool
 
-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/lib.ml b/library/lib.ml
index d4381a6923..a046360822 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -278,7 +278,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 +569,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/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. *)
-- 
cgit v1.2.3


From 63a953ddc0db1ec1bf101ed6afdf9262d0d9f355 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 8 May 2019 21:28:25 +0200
Subject: Ensuring suffix of file to compile also for -vio2vo checking.

We do it by consistently using variants of the "ensure_exists" policy
in compilation modes: vo (default), vio (-quick), vio2vo (-vio2vo) and
parallel vio2vo (schedule-vio2vo), vio checking (-check-vio-tasks) and
parallel vio checking (schedule-vio-checking).

For instance, coqc -vio2vo dir/file.vio now works, while before,
dir/file was expected.

Incidentally, this avoids the non-recommended Loadpath.locate_file.
---
 library/library.ml  | 19 ++++++++-----------
 library/library.mli |  2 +-
 2 files changed, 9 insertions(+), 12 deletions(-)

(limited to 'library')

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


From b1a3ea4855b1e150b2e677a6d5466458893d6c60 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 15 May 2019 18:47:22 +0200
Subject: Inverting the responsibility to define logically a constant in
 Declare.

The code was intricate due to the special handling of side-effects, while
it was sufficient to extrude the logical definition to make it clearer. We
thus declare a constant in two parts, first purely kernel-related, then
purely libobject-related.
---
 library/lib.ml  | 3 ---
 library/lib.mli | 1 -
 2 files changed, 4 deletions(-)

(limited to 'library')

diff --git a/library/lib.ml b/library/lib.ml
index a046360822..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))
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 *)
-- 
cgit v1.2.3


From 93aa8aad110a2839d16dce53af12f0728b59ed2a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 14 May 2019 20:27:24 +0200
Subject: Merge the definition of constants and private constants in the API.

---
 library/global.ml  | 2 +-
 library/global.mli | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'library')

diff --git a/library/global.ml b/library/global.ml
index 06e06a8cf2..33cdbd88ea 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -94,7 +94,7 @@ 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_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)
diff --git a/library/global.mli b/library/global.mli
index a60de48897..f65ffaa2ee 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -46,7 +46,7 @@ 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_mind :
   Id.t -> Entries.mutual_inductive_entry -> MutInd.t
 
-- 
cgit v1.2.3


From 801aed67a90ec49c15a4469e1905aa2835fabe19 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 15 May 2019 23:50:42 +0200
Subject: Parameterize the constant_body type by opaque subproofs.

---
 library/global.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'library')

diff --git a/library/global.mli b/library/global.mli
index f65ffaa2ee..eabae89d8d 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -84,7 +84,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 +105,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 } *)
-- 
cgit v1.2.3


From 27468ae02bbbf018743d53a9db49efa34b6d6a3e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 16 May 2019 00:02:54 +0200
Subject: Ensure statically that declarations built by Term_typing are direct.

This removes a lot of cruft breaking the opaque proof abstraction in
Safe_typing and similar.
---
 library/global.ml  | 1 +
 library/global.mli | 1 +
 2 files changed, 2 insertions(+)

(limited to 'library')

diff --git a/library/global.ml b/library/global.ml
index 33cdbd88ea..58e2380440 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -95,6 +95,7 @@ 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 ?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)
diff --git a/library/global.mli b/library/global.mli
index eabae89d8d..984d8c666c 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -47,6 +47,7 @@ val export_private_constants : in_section:bool ->
 
 val add_constant :
   ?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
 
-- 
cgit v1.2.3