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