diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-12-02 20:19:40 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-12-02 20:19:40 -0500 |
| commit | 727dbeb8f3109e4ac44cef81327ca0dd6f55505e (patch) | |
| tree | 86345c8461a12e86477cf9b9bc1585497a7d01ef /src/Reflection | |
| parent | 215150526079dad408dde1d0744cb0f88765a6ac (diff) | |
Arguments for invert_Pair
Diffstat (limited to 'src/Reflection')
| -rw-r--r-- | src/Reflection/Syntax.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index a88fac743..021e9a21d 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -484,6 +484,7 @@ Global Arguments Interp {_ _ _} interp_op {t} _. Global Arguments interp {_ _ _} interp_op {t} _. Global Arguments interpf {_ _ _} interp_op {t} _. Global Arguments invert_Const {_ _ _ _ _} _. +Global Arguments invert_Pair {_ _ _ _ _ _} _. Module Export Notations. Notation "A * B" := (@Prod _ A B) : ctype_scope. |