diff options
| author |  Jason Gross <jagro@google.com> | 2016-09-05 12:22:53 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-09-05 15:31:28 -0700 |
| commit | 876eb569ba2d315b600adf363ef8fcd4e528d746 (patch) | |
| tree | 640d940d0b584c0b5ea8da7b3cb1907fc0a9432b /src/Reflection | |
| parent | 8029a8bdc4b6f39d72ce0807d856b0ae832a53cb (diff) | |
More 8.4 fixes (apparently rebinding [->] doesn't work)
Diffstat (limited to 'src/Reflection')
| -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). |