From 9d1230d484a2cf519f9cd76dc0f37815f3c6339b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 8 Apr 2017 01:42:19 +0200
Subject: Fix a heuristic used by legacy typeclass resolution.

The evarmap used by the heuristic could contain resolved evars, which could
lead to a failure of backtracking in the EConstr branch. This is experimental
and may be to costly.
---
 tactics/class_tactics.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 7eadde78d5..ea19660931 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -787,10 +787,10 @@ module V85 = struct
              let fk' =
                (fun e ->
                  let do_backtrack =
-                   if unique then occur_existential s' concl
+                   if unique then occur_existential tacgl.sigma concl
                    else if info.unique then true
                    else if List.is_empty gls' then
-                     needs_backtrack env s' info.is_evar concl
+                     needs_backtrack env tacgl.sigma info.is_evar concl
                    else true
                  in
                  let e' = match foundone with None -> e
-- 
cgit v1.2.3