diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Reflection/Syntax.v | 2 |
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). |