From 1fd4c22d493715f154f6b79dc7f6e4efd44ff185 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 17 Nov 2020 18:52:30 +0100
Subject: [ltac] break dependency on the STM

---
 plugins/ltac/profile_ltac.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index aa2449d962..937d579012 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -436,11 +436,7 @@ let finish_timing ~prefix name =
 (* ******************** *)
 
 let print_results_filter ~cutoff ~filter =
-  (* The STM doesn't provide yet a proper document query and traversal
-     API, thus we need to re-check if some states are current anymore
-     (due to backtracking) using the `state_of_id` API. *)
-  let valid (did,id) _ = Stm.(state_of_id ~doc:(get_doc did) id) <> `Expired in
-  data := SM.filter valid !data;
+  data := SM.filter (fun (doc,id) _ -> Stateid.is_valid ~doc id) !data;
   let results =
     SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in
   let results = merge_roots results Local.(CList.last !stack) in
-- 
cgit v1.2.3