From b365304d32db443194b7eaadda63c784814f53f1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sun, 6 Nov 2016 03:23:13 +0100
Subject: Evarconv API using EConstr.

---
 engine/universes.ml | 9 ---------
 1 file changed, 9 deletions(-)

(limited to 'engine/universes.ml')

diff --git a/engine/universes.ml b/engine/universes.ml
index 6720fcef8..51a113219 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -446,15 +446,6 @@ let global_of_constr c =
   | Var id -> VarRef id, Instance.empty
   | _ -> raise Not_found
 
-let global_app_of_constr c =
-  match kind_of_term c with
-  | Const (c, u) -> (ConstRef c, u), None
-  | Ind (i, u) -> (IndRef i, u), None
-  | Construct (c, u) -> (ConstructRef c, u), None
-  | Var id -> (VarRef id, Instance.empty), None
-  | Proj (p, c) -> (ConstRef (Projection.constant p), Instance.empty), Some c
-  | _ -> raise Not_found
-
 open Declarations
 
 let type_of_reference env r =
-- 
cgit v1.2.3