aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection/Syntax.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2016-12-02 18:25:27 -0500
committerGravatar Jason Gross <jgross@mit.edu>2016-12-02 18:25:27 -0500
commit118f2039566db61cb5ea6158bdf531bd0a4faffd (patch)
treedaf83649898abed06c9732e0d421b7253b78552e /src/Reflection/Syntax.v
parent8962d85902089a657aa06a39e50355c7c4c787da (diff)
SmartFlatTypeMap arguments
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 cd20c78a0..4ee9b8087 100644
--- a/src/Reflection/Syntax.v
+++ b/src/Reflection/Syntax.v
@@ -430,6 +430,7 @@ Global Arguments SmartVarf {_ _ _ _ _} _.
Global Arguments SmartValf {_} T _ t.
Global Arguments SmartVarVarf {_ _ _ _ _} _.
Global Arguments SmartVarfMap {_ _ _} _ {_} _.
+Global Arguments SmartFlatTypeMap {_ _} _ {_} _.
Global Arguments SmartVarMap_hetero {_ _ _ _ _} _ _ {_} _.
Global Arguments SmartVarMap {_ _ _} _ _ {_} _.
Global Arguments SmartConstf {_ _ _ _ _} _.