diff options
| author |  Jason Gross <jagro@google.com> | 2016-09-05 10:50:45 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-09-05 15:31:28 -0700 |
| commit | 7aeb1054f646c838b109b27160e224191ac75bd4 (patch) | |
| tree | 5b0068050328d5bcb45ed9e9c4965076f9f21de0 /src/Reflection/Syntax.v | |
| parent | 28fc98d1caa4bad57ea13cce3715062f892c5f78 (diff) | |
Fix for 8.4 compatibility
Diffstat (limited to 'src/Reflection/Syntax.v')
| -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 a60f0d76f..d13eb1a42 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -64,7 +64,7 @@ Section language. Bind Scope expr_scope with exprf. Inductive expr : type -> Type := | Return {t} : exprf t -> expr t - | Abs {src dst} : (var src -> expr dst) -> expr (src -> dst). + | Abs {src dst} : (var src -> expr dst) -> expr (Arrow src dst). Bind Scope expr_scope with expr. Global Coercion Return : exprf >-> expr. Fixpoint smart_interp_flat_map {f g} |