aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/declaremods.mli2
-rw-r--r--library/global.ml6
-rw-r--r--library/global.mli7
-rw-r--r--library/goptions.ml10
-rw-r--r--library/goptions.mli9
-rw-r--r--library/keys.mli2
-rw-r--r--library/libnames.mli9
-rw-r--r--library/nameops.mli8
-rw-r--r--library/nametab.mli3
9 files changed, 28 insertions, 28 deletions
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 1f2aaf7b54..005594b8d8 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -121,7 +121,7 @@ val iter_all_segments :
(Libnames.object_name -> Libobject.obj -> unit) -> unit
-val debug_print_modtab : unit -> Pp.std_ppcmds
+val debug_print_modtab : unit -> Pp.t
(** For printing modules, [process_module_binding] adds names of
bound module (and its components) to Nametab. It also loads
diff --git a/library/global.ml b/library/global.ml
index 5b17855dce..963c977417 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -86,6 +86,7 @@ let push_context b c = globalize0 (Safe_typing.push_context b c)
let set_engagement c = globalize0 (Safe_typing.set_engagement c)
let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c)
+let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd)
let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d)
let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie)
let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
@@ -198,8 +199,7 @@ let type_of_global_in_context env r =
| ConstRef c ->
let cb = Environ.lookup_constant c env in
let univs = Declareops.constant_polymorphic_context cb in
- let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in
- Typeops.type_of_constant_type env cb.Declarations.const_type, univs
+ cb.Declarations.const_type, univs
| IndRef ind ->
let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
let univs = Declareops.inductive_polymorphic_context mib in
@@ -254,7 +254,7 @@ let is_template_polymorphic r =
let env = env() in
match r with
| VarRef id -> false
- | ConstRef c -> Environ.template_polymorphic_constant c env
+ | ConstRef c -> false
| IndRef ind -> Environ.template_polymorphic_ind ind env
| ConstructRef cstr -> Environ.template_polymorphic_ind (inductive_of_constructor cstr) env
diff --git a/library/global.mli b/library/global.mli
index 48bcfa989f..c777691d11 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -34,9 +34,12 @@ val set_typing_flags : Declarations.typing_flags -> unit
val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit
val push_named_def : (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.universe_context_set
+val export_private_constants : in_section:bool ->
+ Safe_typing.private_constants Entries.constant_entry ->
+ unit Entries.constant_entry * Safe_typing.exported_private_constant list
+
val add_constant :
- DirPath.t -> Id.t -> Safe_typing.global_declaration ->
- constant * Safe_typing.exported_private_constant list
+ DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant
val add_mind :
DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> mutual_inductive
diff --git a/library/goptions.ml b/library/goptions.ml
index fe014ef68e..184c6fa119 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -57,10 +57,10 @@ module MakeTable =
val table : (string * key table_of_A) list ref
val encode : key -> t
val subst : substitution -> t -> t
- val printer : t -> std_ppcmds
+ val printer : t -> Pp.t
val key : option_name
val title : string
- val member_message : t -> bool -> std_ppcmds
+ val member_message : t -> bool -> Pp.t
end) ->
struct
type option_mark =
@@ -131,7 +131,7 @@ module type StringConvertArg =
sig
val key : option_name
val title : string
- val member_message : string -> bool -> std_ppcmds
+ val member_message : string -> bool -> Pp.t
end
module StringConvert = functor (A : StringConvertArg) ->
@@ -161,10 +161,10 @@ sig
val compare : t -> t -> int
val encode : reference -> t
val subst : substitution -> t -> t
- val printer : t -> std_ppcmds
+ val printer : t -> Pp.t
val key : option_name
val title : string
- val member_message : t -> bool -> std_ppcmds
+ val member_message : t -> bool -> Pp.t
end
module RefConvert = functor (A : RefConvertArg) ->
diff --git a/library/goptions.mli b/library/goptions.mli
index 3100c1ce72..cec7250f1f 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -43,7 +43,6 @@
All options are synchronized with the document.
*)
-open Pp
open Libnames
open Mod_subst
@@ -64,7 +63,7 @@ module MakeStringTable :
(A : sig
val key : option_name
val title : string
- val member_message : string -> bool -> std_ppcmds
+ val member_message : string -> bool -> Pp.t
end) ->
sig
val active : string -> bool
@@ -88,10 +87,10 @@ module MakeRefTable :
val compare : t -> t -> int
val encode : reference -> t
val subst : substitution -> t -> t
- val printer : t -> std_ppcmds
+ val printer : t -> Pp.t
val key : option_name
val title : string
- val member_message : t -> bool -> std_ppcmds
+ val member_message : t -> bool -> Pp.t
end) ->
sig
val active : A.t -> bool
@@ -177,6 +176,6 @@ type option_state = {
}
val get_tables : unit -> option_state OptionMap.t
-val print_tables : unit -> std_ppcmds
+val print_tables : unit -> Pp.t
val error_undeclared_key : option_name -> 'a
diff --git a/library/keys.mli b/library/keys.mli
index 6fe9efc6ec..d5dc0e2a1f 100644
--- a/library/keys.mli
+++ b/library/keys.mli
@@ -19,5 +19,5 @@ val equiv_keys : key -> key -> bool
val constr_key : ('a -> ('a, 't, 'u, 'i) Constr.kind_of_term) -> 'a -> key option
(** Compute the head key of a term. *)
-val pr_keys : (global_reference -> Pp.std_ppcmds) -> Pp.std_ppcmds
+val pr_keys : (global_reference -> Pp.t) -> Pp.t
(** Pretty-print the mapping *)
diff --git a/library/libnames.mli b/library/libnames.mli
index b6d6f7f3bc..1b351290a4 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -7,14 +7,13 @@
(************************************************************************)
open Util
-open Pp
open Loc
open Names
(** {6 Dirpaths } *)
(** FIXME: ought to be in Names.dir_path *)
-val pr_dirpath : DirPath.t -> Pp.std_ppcmds
+val pr_dirpath : DirPath.t -> Pp.t
val dirpath_of_string : string -> DirPath.t
val string_of_dirpath : DirPath.t -> string
@@ -58,7 +57,7 @@ val basename : full_path -> Id.t
(** Parsing and printing of section path as ["coq_root.module.id"] *)
val path_of_string : string -> full_path
val string_of_path : full_path -> string
-val pr_path : full_path -> std_ppcmds
+val pr_path : full_path -> Pp.t
module Spmap : CSig.MapS with type key = full_path
@@ -77,7 +76,7 @@ val repr_qualid : qualid -> DirPath.t * Id.t
val qualid_eq : qualid -> qualid -> bool
-val pr_qualid : qualid -> std_ppcmds
+val pr_qualid : qualid -> Pp.t
val string_of_qualid : qualid -> string
val qualid_of_string : string -> qualid
@@ -124,7 +123,7 @@ type reference =
val eq_reference : reference -> reference -> bool
val qualid_of_reference : reference -> qualid located
val string_of_reference : reference -> string
-val pr_reference : reference -> std_ppcmds
+val pr_reference : reference -> Pp.t
val loc_of_reference : reference -> Loc.t option
val join_reference : reference -> reference -> reference
diff --git a/library/nameops.mli b/library/nameops.mli
index 88290f4850..89aba24476 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -106,13 +106,13 @@ val name_max : Name.t -> Name.t -> Name.t
val name_cons : Name.t -> Id.t list -> Id.t list
(** @deprecated Same as [Name.cons] *)
-val pr_name : Name.t -> Pp.std_ppcmds
+val pr_name : Name.t -> Pp.t
(** @deprecated Same as [Name.print] *)
-val pr_id : Id.t -> Pp.std_ppcmds
+val pr_id : Id.t -> Pp.t
(** @deprecated Same as [Names.Id.print] *)
-val pr_lab : Label.t -> Pp.std_ppcmds
+val pr_lab : Label.t -> Pp.t
(** some preset paths *)
@@ -127,5 +127,5 @@ val coq_string : string (** "Coq" *)
val default_root_prefix : DirPath.t
(** Metavariables *)
-val pr_meta : Term.metavariable -> Pp.std_ppcmds
+val pr_meta : Term.metavariable -> Pp.t
val string_of_meta : Term.metavariable -> string
diff --git a/library/nametab.mli b/library/nametab.mli
index be57f5dcc6..025a63b1ce 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pp
open Names
open Libnames
open Globnames
@@ -155,7 +154,7 @@ val basename_of_global : global_reference -> Id.t
(** Printing of global references using names as short as possible.
@raise Not_found when the reference is not in the global tables. *)
-val pr_global_env : Id.Set.t -> global_reference -> std_ppcmds
+val pr_global_env : Id.Set.t -> global_reference -> Pp.t
(** The [shortest_qualid] functions given an object with [user_name]
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 20:50:18 +0000