From 1b029b2163386f20179a61f6bdb68e5532f4c306 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sat, 24 Oct 2015 12:01:26 +0200
Subject: Fixing a loop in checking hints with holes.

For instance, "Hint Resolve (fst _ _)." was looping (bug in 841bc461).
---
 tactics/hints.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 2755ed9cb..4ba9adafe 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1071,7 +1071,7 @@ let prepare_hint check (poly,local) env init (sigma,c) =
       (* We skip the test whether args is the identity or not *)
       let t = Evarutil.nf_evar sigma (existential_type sigma ev) in
       let t = List.fold_right (fun (e,id) c -> replace_term e id c) !subst t in
-      if not (Int.Set.is_empty (free_rels t)) then
+      if not (closed0 c) then
 	error "Hints with holes dependent on a bound variable not supported.";
       if occur_existential t then
 	(* Not clever enough to construct dependency graph of evars *)
-- 
cgit v1.2.3