aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/global.ml4
-rw-r--r--library/global.mli4
2 files changed, 0 insertions, 8 deletions
diff --git a/library/global.ml b/library/global.ml
index dd7f23378..8b59c84dd 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -124,10 +124,6 @@ let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ())
let opaque_tables () = Environ.opaque_tables (env ())
let body_of_constant_body cb = Declareops.body_of_constant (opaque_tables ()) cb
let body_of_constant cst = body_of_constant_body (lookup_constant cst)
-let constraints_of_constant_body cb =
- Declareops.constraints_of_constant (opaque_tables ()) cb
-let universes_of_constant_body cb =
- Declareops.universes_of_constant (opaque_tables ()) cb
(** Operations on kernel names *)
diff --git a/library/global.mli b/library/global.mli
index c7ccabe1a..754fa1516 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -91,10 +91,6 @@ val mind_of_delta_kn : kernel_name -> mutual_inductive
val opaque_tables : unit -> Opaqueproof.opaquetab
val body_of_constant : constant -> Term.constr option
val body_of_constant_body : Declarations.constant_body -> Term.constr option
-val constraints_of_constant_body :
- Declarations.constant_body -> Univ.constraints
-val universes_of_constant_body :
- Declarations.constant_body -> Univ.universe_context
(** Global universe name <-> level mapping *)
type universe_names =