diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-12-03 14:55:14 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-12-03 14:55:14 -0500 |
| commit | 827683317a098a5436a837760573a59ce6e43420 (patch) | |
| tree | 83e71e9a54f17431b5e589271736c0d1afa6723c /src/Reflection | |
| parent | 726a3345d37f9e45c9ab660cb73334f18a88cb77 (diff) | |
Arguments for invert_Op
Diffstat (limited to 'src/Reflection')
| -rw-r--r-- | src/Reflection/Syntax.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index 40b7cdbc5..80c487687 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -500,8 +500,9 @@ 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 {_ _ _ _ _ _} _. +Global Arguments invert_Op {_ _ _ _ _} _. Global Arguments invert_LetIn {_ _ _ _ _} _. +Global Arguments invert_Pair {_ _ _ _ _ _} _. Module Export Notations. Notation "A * B" := (@Prod _ A B) : ctype_scope. |