Commit 468d8467 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Projection notation at level 8 for Coq 8.6

parent d7d7b30b
Pipeline #10606 passed with stage
in 2 minutes and 28 seconds
......@@ -91,7 +91,7 @@ Module RecordSetNotations.
Delimit Scope record_set with rs.
Open Scope rs.
Notation "x [ proj := v ]" := (set proj (constructor v) x)
(at level 10, left associativity) : record_set.
(at level 8, left associativity) : record_set.
Notation "x [ proj ::= f ]" := (set proj f x)
(at level 10, f at next level, left associativity) : record_set.
(at level 8, 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