From 58630ad9a0b94a804a39a3d99f982965292692c7 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 21 May 2018 23:54:55 +0200
Subject: [api] Misctypes removal: miscellaneous aliases.

---
 pretyping/typeclasses.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/typeclasses.mli')

diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index c78382c822..e4a56960cf 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -21,7 +21,7 @@ type 'a hint_info_gen =
     { hint_priority : int option;
       hint_pattern : 'a option }
 
-type hint_info = (Misctypes.patvar list * Pattern.constr_pattern) hint_info_gen
+type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen
 
 (** This module defines type-classes *)
 type typeclass = {
-- 
cgit v1.2.3