diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-14 22:26:55 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-05-14 22:26:55 -0400 |
| commit | 72a84fc5e7e7835608ad722c6c1a79e7067cc4a9 (patch) | |
| tree | 372d3849c4140c155ec7d51754e62f1182bd0603 /src | |
| parent | 725f694d9bad0202c0ed1ac367b624bdd9a974c0 (diff) | |
Add a reserved C notation
Diffstat (limited to 'src')
| -rw-r--r-- | src/Compilers/Z/CNotations.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Compilers/Z/CNotations.v b/src/Compilers/Z/CNotations.v index 7503f6c34..80d1e17c9 100644 --- a/src/Compilers/Z/CNotations.v +++ b/src/Compilers/Z/CNotations.v @@ -9,6 +9,7 @@ Reserved Notation "T x = A ; 'return' ( b0 , b1 , .. , b2 )" (at level 200, form Reserved Notation "T0 x , T1 y = A ; b" (at level 200, b at level 200, format "T0 x , T1 y = A ; '//' b"). Reserved Notation "T0 x , T1 y = A ; 'return' b" (at level 200, b at level 200, format "T0 x , T1 y = A ; '//' 'return' b"). Reserved Notation "T0 x , T1 y = A ; 'return' ( b0 , b1 , .. , b2 )" (at level 200, format "T0 x , T1 y = A ; '//' 'return' ( b0 , b1 , .. , b2 )"). +Reserved Notation "v == 0 ? a : b" (at level 40, a at level 10, b at level 10). Reserved Notation "x & y" (at level 40). Global Open Scope expr_scope. |