diff options
| -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. |