Skip to content
Snippets Groups Projects
Commit 45bb2a9f authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] force step indexing before strategies

parent b66edb93
No related branches found
No related tags found
No related merge requests found
...@@ -89,8 +89,10 @@ let search tree ?anchor ?sequent heuristics = ...@@ -89,8 +89,10 @@ let search tree ?anchor ?sequent heuristics =
let anchor = ProofEngine.anchor tree ?node:anchor () in let anchor = ProofEngine.anchor tree ?node:anchor () in
let sequent = let sequent =
match sequent with match sequent with
| Some s -> s | None -> snd (Wpo.compute (ProofEngine.goal anchor)) in | Some s -> s
| None -> snd (Wpo.compute (ProofEngine.goal anchor)) in
let lookup h = try h#search pool#add sequent with Not_found -> () in let lookup h = try h#search pool#add sequent with Not_found -> () in
Conditions.index sequent ;
WpContext.on_context WpContext.on_context
(ProofEngine.node_context anchor) (ProofEngine.node_context anchor)
(List.iter lookup) heuristics ; (List.iter lookup) heuristics ;
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment