diff options
author | Jason Gross <jgross@mit.edu> | 2017-10-10 00:45:03 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-10-10 01:24:18 -0400 |
commit | 5c97e8f6ad95175be18ddf4ee308d45e555c8fb7 (patch) | |
tree | 6b9692ce0575e5225913686204633f2f500c76a6 | |
parent | 02d652bc54fb5629d8f4caa731148a7cf0393c04 (diff) |
TagList: make get error, and fix bugs
-rw-r--r-- | src/Util/TagList.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/Util/TagList.v b/src/Util/TagList.v index b2d86e93f..e5f20afe2 100644 --- a/src/Util/TagList.v +++ b/src/Util/TagList.v @@ -40,9 +40,9 @@ Module Tag. lazymatch (eval hnf in ctx) with | context[{| key := key' ; value := ?value' |}] => tac_found value' - | context[add_gen ?key' ?value' _ _] => tac_found value' - | context[add_local ?key' ?value' _] => tac_found value' - | context[add ?key' ?value' _] => tac_found value' + | context[add_gen key' ?value' _ _] => tac_found value' + | context[add_local key' ?value' _] => tac_found value' + | context[add key' ?value' _] => tac_found value' | _ => lazymatch allow_unfound with | true => tac_not_found () end @@ -60,8 +60,9 @@ Module Tag. Ltac get_error ctx key' := get_gen_cont ctx key' ltac:(fun v => v) ltac:(fun _ => constr:(I)) false. + Ltac get_default ctx key' := get_gen ctx key' ltac:(fun _ => constr:(I)). - Ltac get ctx key' := get_gen ctx key' ltac:(fun _ => constr:(I)). + Ltac get ctx key' := get_error ctx key'. Notation get ctx key' := ltac:(let v := get ctx key' in exact v) (only parsing). |