diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-01-03 13:12:21 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-01-03 13:12:21 -0500 |
| commit | a6432f29a29cfb802a1eba164244418a930f7797 (patch) | |
| tree | 18f6db3eaded6ada017587b28d38ac22b9025d92 /src/Reflection/MultiSizeTest2.v | |
| parent | 3e57994ff4fd1870550e78bfbf6a2d4ac8b462a6 (diff) | |
Fixes for Coq 8.4
Diffstat (limited to 'src/Reflection/MultiSizeTest2.v')
| -rw-r--r-- | src/Reflection/MultiSizeTest2.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Reflection/MultiSizeTest2.v b/src/Reflection/MultiSizeTest2.v index 32591fc2f..a0c9fc864 100644 --- a/src/Reflection/MultiSizeTest2.v +++ b/src/Reflection/MultiSizeTest2.v @@ -157,7 +157,7 @@ Example ex1 : Expr base_type interp_base_type op TNat := fun var => LetIn (Op (tR:=TNat) (Plus Nat) (Pair (Var a) (Var b))) (fun c : var Nat => Op (Plus Nat) (Pair (Var c) (Var c))))). -Example ex1f : Expr base_type interp_base_type op (Nat -> Nat -> TNat) := fun var => +Example ex1f : Expr base_type interp_base_type op (Arrow Nat (Arrow Nat TNat)) := fun var => Abs (fun a0 => Abs (fun b0 => LetIn (Var a0) (fun a : var Nat => |