Add update_by_tac_if_not_exists

1 files changed, 6 insertions, 2 deletions

diff --git a/src/Util/TagList.v b/src/Util/TagList.v
index e5f20afe2..802b7ad92 100644
--- a/src/Util/TagList.v
+++ b/src/Util/TagList.v
@@ -48,13 +48,17 @@ Module Tag.
            end
     end.
 
-  Ltac update_if_not_exists ctx key value :=
+  Ltac update_by_tac_if_not_exists ctx key value_tac :=
     get_gen_cont
       ctx key
       ltac:(fun value' => ctx)
-             ltac:(fun _ => update ctx key value)
+             ltac:(fun _ => let value := value_tac () in
+                            update ctx key value)
                     true.
 
+  Ltac update_if_not_exists ctx key value :=
+    update_by_tac_if_not_exists ctx key ltac:(fun _ => value).
+
   Ltac get_gen ctx key' default :=
     get_gen_cont ctx key' ltac:(fun v => v) default true.