diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-03-02 10:58:28 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-03-02 13:37:14 -0500 |
| commit | 0ab98d3380033b58162015656f435ae90b936856 (patch) | |
| tree | 38a17503ccbc5fd51d473f458e782812360ed5b1 /src/Reflection/Syntax.v | |
| parent | 7f0ba34481f59db0cf430d7a08b8b65d953eb803 (diff) | |
make 8.5 happy
Diffstat (limited to 'src/Reflection/Syntax.v')
| -rw-r--r-- | src/Reflection/Syntax.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index d77731633..d8b88e560 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -134,10 +134,10 @@ Global Arguments interp_type_gen_hetero {_} _ _ _. Global Arguments interp_type_gen {_} _ _. Global Arguments interp_flat_type {_} _ _. Global Arguments interp_type {_} _ _. -Global Arguments Interp {_ _ _} interp_op {t} _. -Global Arguments interp {_ _ _} interp_op {t} _. +Global Arguments Interp {_ _ _} interp_op {t} _ _. +Global Arguments interp {_ _ _} interp_op {t} _ _. Global Arguments interpf {_ _ _} interp_op {t} _. -Global Arguments interp _ _ _ _ _ !_ / . +Global Arguments interp _ _ _ _ _ !_ / _. Module Export Notations. Notation "()" := (@Unit _) : ctype_scope. |