From e2c0cd1cb7fd06ef37f87f64e1164766820c16ea Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 15 Sep 2014 12:12:41 +0200
Subject: Avoid backtracking in typeclass search if a solution for a closed
 non-dependent or propositional constraint has already been found (same
 behavior as before previous patch).

---
 tactics/class_tactics.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 29cc6f51ac..77101c70e6 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -442,7 +442,14 @@ let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk
 	 | _ ->
 	     second.skft
 	       (fun {it=gls';sigma=s'} fk' -> 
-		 aux s' (gls'::acc) fk' gls)
+		 let fk'' =
+		   if not info.unique && List.is_empty gls' &&
+		     not (needs_backtrack (Goal.V82.env s gl) s
+			    info.is_evar (Goal.V82.concl s gl))
+		   then fk
+		   else fk'
+		 in
+		   aux s' (gls'::acc) fk'' gls)
 	       fk {it = (gl,info); sigma = s; })
     | [] -> Somek2 (List.rev acc, s, fk)
   in fun {it = gls; sigma = s; } fk ->
-- 
cgit v1.2.3