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 --- lib/stateid.ml | 3 +++ 1 file changed, 3 insertions(+) (limited to 'lib/stateid.ml') diff --git a/lib/stateid.ml b/lib/stateid.ml index a1328f156c..2a41cb7866 100644 --- a/lib/stateid.ml +++ b/lib/stateid.ml @@ -45,3 +45,6 @@ type ('a,'b) request = { name : string } +let is_valid_ref = ref (fun ~doc:_ (_ : t) -> true) +let is_valid ~doc id = !is_valid_ref ~doc id +let set_is_valid f = is_valid_ref := f -- cgit v1.2.3