From 07f4e6b07775052cc1c5dc34cdfa7ad4eacfa94f Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sun, 4 Oct 2015 14:50:45 +0200
Subject: Fix bug #4354: interpret hints in the right env and sigma.

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

(limited to 'tactics/hints.mli')

diff --git a/tactics/hints.mli b/tactics/hints.mli
index 687bc78c76..5a4fb77091 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -93,8 +93,8 @@ module Hint_db :
 	arguments. *)
     val map_auto : (global_reference * constr array) -> constr -> t -> full_hint list
 
-    val add_one : hint_entry -> t -> t
-    val add_list : (hint_entry) list -> t -> t
+    val add_one : env -> evar_map -> hint_entry -> t -> t
+    val add_list : env -> evar_map -> hint_entry list -> t -> t
     val remove_one : global_reference -> t -> t
     val remove_list : global_reference list -> t -> t
     val iter : (global_reference option -> bool array list -> full_hint list -> unit) -> t -> unit
-- 
cgit v1.2.3