From 65c0573cf7dda899374122e0dc558c551223bc00 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 10 Oct 2017 03:04:57 -0400 Subject: Add update_by_tac_if_not_exists --- src/Util/TagList.v | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'src/Util/TagList.v') 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. -- cgit v1.2.3