From 46c0b7ab3653a6f1ef4b40466c2dd130d09136cb Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 11 Jun 2020 18:51:34 +0200
Subject: Move given_up goals to evar_map

---
 tactics/class_tactics.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 31132824f5..597e60093b 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -967,9 +967,7 @@ module Search = struct
            let evm' = Evd.set_typeclass_evars evm' nongoals' in
              Some evm'
         in
-        let (), pv', (unsafe, shelved, gaveup), _ = Proofview.apply ~name ~poly env tac pv in
-        if not (List.is_empty gaveup) then
-          CErrors.anomaly (Pp.str "run_on_evars not assumed to apply tactics generating given up goals.");
+        let (), pv', (unsafe, shelved), _ = Proofview.apply ~name ~poly env tac pv in
         if Proofview.finished pv' then finish pv' shelved
         else raise Not_found
        with Logic_monad.TacticFailure _ -> raise Not_found
-- 
cgit v1.2.3