TagList: make get error, and fix bugs

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).