diff options
Diffstat (limited to 'src/Reflection/InputSyntax.v')
| -rw-r--r-- | src/Reflection/InputSyntax.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Reflection/InputSyntax.v b/src/Reflection/InputSyntax.v index 1c97d2174..5d1500d20 100644 --- a/src/Reflection/InputSyntax.v +++ b/src/Reflection/InputSyntax.v @@ -134,3 +134,4 @@ Global Arguments MatchPair {_ _ _ _ _ _} _ {_} _. Global Arguments Pair {_ _ _ _ _} _ {_} _. Global Arguments Return {_ _ _ _ _} _. Global Arguments Abs {_ _ _ _ _ _} _. +Global Arguments Compile {_ _ _ t} _ _. |