aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Reflection/Linearize.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Reflection/Linearize.v b/src/Reflection/Linearize.v
index d7d1fc2b6..77b927b56 100644
--- a/src/Reflection/Linearize.v
+++ b/src/Reflection/Linearize.v
@@ -97,6 +97,7 @@ Section language.
:= fun var => inline_const (e _).
End language.
+Global Arguments under_letsf {_ _ _ _ _} _ {tC} _.
Global Arguments linearizef {_ _ _ _ _} _.
Global Arguments linearize {_ _ _ _ _} _.
Global Arguments Linearize {_ _ _ _} _ var.