From 91172e9c3a1430c3be3ad1080d2da68b25d940aa Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 12 Apr 2015 21:13:51 +0200
Subject: Making the hint entry type opaque.

---
 tactics/hints.mli | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/tactics/hints.mli b/tactics/hints.mli
index 42379b7c0c..9a781c722c 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -54,8 +54,7 @@ type search_entry
 
 (** The head may not be bound. *)
 
-type hint_entry = global_reference option * 
-  (constr * types * Univ.universe_context_set) gen_auto_tactic
+type hint_entry
 
 type hints_path =
   | PathAtom of hints_path_atom
-- 
cgit v1.2.3