Merge PR #6676: [proofview] goals come with a state

1 files changed, 3 insertions, 1 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index a95e6b941..8284c4939 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1131,6 +1131,7 @@ module Search = struct
       let rec result (shelf, ()) i k =
         foundone := true;
         Proofview.Unsafe.tclGETGOALS >>= fun gls ->
+        let gls = CList.map Proofview.drop_state gls in
         let j = List.length gls in
         (if !typeclasses_debug > 0 then
            Feedback.msg_debug
@@ -1179,7 +1180,7 @@ module Search = struct
               (if List.is_empty goals then tclUNIT ()
                else
 	         let sigma' = mark_unresolvables sigma goals in
-	         with_shelf (Unsafe.tclEVARS sigma' <*> Unsafe.tclNEWGOALS goals) >>=
+                 with_shelf (Unsafe.tclEVARS sigma' <*> Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state goals)) >>=
                       fun s -> result s i (Some (Option.default 0 k + j)))
           end
         in with_shelf res >>= fun (sh, ()) ->
@@ -1272,6 +1273,7 @@ module Search = struct
           search_tac_gl ~st only_classes dep hints depth (succ i) sigma gls gl end
     in
       Proofview.Unsafe.tclGETGOALS >>= fun gls ->
+      let gls = CList.map Proofview.drop_state gls in
       Proofview.tclEVARMAP >>= fun sigma ->
       let j = List.length gls in
       (tclDISPATCH (List.init j (fun i -> tac sigma gls i)))