Commit 98d7ce9b authored by Robbert Krebbers's avatar Robbert Krebbers

Fix the match notation in heap_lang for option.

parent 859794e3
......@@ -114,6 +114,6 @@ Notation SOMEV x := (InjRV x).
Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" :=
(Match e0 BAnon e1 x%bind e2)
(e0, e1, x, e2 at level 200) : expr_scope.
Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 | 'end'" :=
Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" :=
(Match e0 BAnon e1 x%bind e2)
(e0, e1, x, e2 at level 200, only parsing) : expr_scope.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment