From e500c71e46e6ff252455b9698addedb101662994 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 11 Oct 2019 12:45:53 +0000
Subject: [engine] Remove UnivGen.global_of_constr

---
 engine/univGen.ml  | 8 --------
 engine/univGen.mli | 3 ---
 2 files changed, 11 deletions(-)

(limited to 'engine')

diff --git a/engine/univGen.ml b/engine/univGen.ml
index b1ed3b2694..1fe09270ba 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -82,14 +82,6 @@ let fresh_global_or_constr_instance env = function
   | IsConstr c -> c, ContextSet.empty
   | IsGlobal gr -> fresh_global_instance env gr
 
-let global_of_constr c =
-  match kind c with
-  | Const (c, u) -> GlobRef.ConstRef c, u
-  | Ind (i, u) -> GlobRef.IndRef i, u
-  | Construct (c, u) -> GlobRef.ConstructRef c, u
-  | Var id -> GlobRef.VarRef id, Instance.empty
-  | _ -> raise Not_found
-
 let fresh_sort_in_family = function
   | InSProp -> Sorts.sprop, ContextSet.empty
   | InProp -> Sorts.prop, ContextSet.empty
diff --git a/engine/univGen.mli b/engine/univGen.mli
index 1c8735bfa8..1b351c61c4 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -54,9 +54,6 @@ val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_const
 val fresh_universe_context_set_instance : ContextSet.t ->
   universe_level_subst * ContextSet.t
 
-(** Raises [Not_found] if not a global reference. *)
-val global_of_constr : constr -> GlobRef.t puniverses
-
 (** Create a fresh global in the global environment, without side effects.
     BEWARE: this raises an error on polymorphic constants/inductives:
     the constraints should be properly added to an evd.
-- 
cgit v1.2.3