Commit 72a21a50 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Make sure record-update notation does not conflict

parent 0f061471
......@@ -90,8 +90,8 @@ Hint Extern 1 (Setter _) => SetInstance_t : typeclass_instances.
Module RecordSetNotations.
Delimit Scope record_set with rs.
Open Scope rs.
Notation "x [ proj := v ]" := (set proj (constructor v) x)
Notation "x [[ proj := v ]]" := (set proj (constructor v) x)
(at level 12, left associativity) : record_set.
Notation "x [ proj ::= f ]" := (set proj f x)
Notation "x [[ proj ::= f ]]" := (set proj f x)
(at level 12, f at next level, left associativity) : record_set.
End RecordSetNotations.
Supports Markdown
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