aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection/Syntax.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Reflection/Syntax.v')
-rw-r--r--src/Reflection/Syntax.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v
index 7df4c2a4d..4e650203c 100644
--- a/src/Reflection/Syntax.v
+++ b/src/Reflection/Syntax.v
@@ -293,6 +293,7 @@ Global Arguments SmartVar {_ _ _ _ _} _.
Global Arguments SmartVal {_} T _ t.
Global Arguments SmartVarVar {_ _ _ _ _} _.
Global Arguments SmartVarMap {_ _ _} _ {_} _.
+Global Arguments SmartVarMapT {_ _ _} _ _ {_} _.
Global Arguments SmartConst {_ _ _ _ _} _.
Global Arguments Op {_ _ _ _ _ _} _ _.
Global Arguments LetIn {_ _ _ _ _} _ {_} _.