aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection
diff options
context:
space:
mode:
Diffstat (limited to 'src/Reflection')
-rw-r--r--src/Reflection/Syntax.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v
index d13eb1a42..8e4274559 100644
--- a/src/Reflection/Syntax.v
+++ b/src/Reflection/Syntax.v
@@ -164,7 +164,7 @@ Section language.
| WfReturn : forall t G e e', @wff G t e e' -> wf G (Return e) (Return e')
| WfAbs : forall A B G e e',
(forall x x', @wf ((x == x') :: G) B (e x) (e' x'))
- -> @wf G (A -> B) (Abs e) (Abs e').
+ -> @wf G (Arrow A B) (Abs e) (Abs e').
End wf.
Definition Wf {t} (E : @Expr t) := forall var1 var2, wf nil (E var1) (E var2).