aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-01-22 17:35:02 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-02-20 14:44:58 +0100
commit041ee4822cb247e60df51fa147175f8b16711df1 (patch)
tree49e61993afab55d44d9642f5dcaebf36fa6cd94b /tactics
parentaec63ba9c8f6840d98ba731640a786138d836343 (diff)
proofview: goals come with a state
Diffstat (limited to 'tactics')
-rw-r--r--tactics/class_tactics.ml4
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)))