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 | |
| parent | 3e57994ff4fd1870550e78bfbf6a2d4ac8b462a6 (diff) | |
Fixes for Coq 8.4
Diffstat (limited to 'src/Reflection')
| -rw-r--r-- | src/Reflection/MapCast.v | 1 | ||||
| -rw-r--r-- | src/Reflection/MultiSizeTest2.v | 2 |
2 files changed, 2 insertions, 1 deletions
diff --git a/src/Reflection/MapCast.v b/src/Reflection/MapCast.v index d84515cb0..a557aec1c 100644 --- a/src/Reflection/MapCast.v +++ b/src/Reflection/MapCast.v @@ -98,6 +98,7 @@ Section language. | Pair _ _ _ _, _ => @failf _ end. + Arguments mapf_interp_cast {_} _ {_} _. (* 8.4 workaround for bad arguments *) Fixpoint map_interp_cast {t1} (e1 : @expr base_type_code1 interp_base_type1 op1 ivarf t1) 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 => |