From af788fd0daeed459b98ed9acd3a0443f53666176 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Feb 2020 17:52:29 +0100
Subject: unsafe_type_of -> type_of in Sequent.extend_with_auto_hints

+ fix evar leak in caller
---
 tactics/hints.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'tactics')

diff --git a/tactics/hints.mli b/tactics/hints.mli
index 2a9b71387e..9c9f0b7708 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -160,6 +160,8 @@ module Hint_db :
     val iter : (GlobRef.t option ->
                 hint_mode array list -> full_hint list -> unit) -> t -> unit
 
+    val fold : (GlobRef.t option -> hint_mode array list -> full_hint list -> 'a -> 'a) -> t -> 'a -> 'a
+
     val use_dn : t -> bool
     val transparent_state : t -> TransparentState.t
     val set_transparent_state : t -> TransparentState.t -> t
-- 
cgit v1.2.3