From 36a98d55576ebdb106a55c3bd682961da8d77dee Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 21 May 2018 23:57:32 +0200
Subject: [api] Misctypes removal: remove dummy alias.

---
 library/misctypes.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'library')

diff --git a/library/misctypes.ml b/library/misctypes.ml
index 3b629f449f..7cd1a83be1 100644
--- a/library/misctypes.ml
+++ b/library/misctypes.ml
@@ -38,10 +38,6 @@ type 'id move_location =
   | MoveFirst
   | MoveLast (** can be seen as "no move" when doing intro *)
 
-(** A synonym of [Evar.t], also defined in Term *)
-
-type existential_key = Evar.t
-
 (** Casts *)
 
 type 'a cast_type =
-- 
cgit v1.2.3