aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-02-08 19:07:43 -0500
committerGravatar Jason Gross <jgross@mit.edu>2017-02-08 19:07:48 -0500
commit430e03ee9034e1197fd95f91f566ac92d70b8c65 (patch)
tree2c771a54515e5a7941c53d58ef926091777aef74
parent1701df710e52d4d4e6e97e608c09cfd80d7b7d8c (diff)
Fix type inference bug in 8.6
-rw-r--r--src/Reflection/MultiSizeTest2.v4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/Reflection/MultiSizeTest2.v b/src/Reflection/MultiSizeTest2.v
index 0b8c7f958..e50b75ecd 100644
--- a/src/Reflection/MultiSizeTest2.v
+++ b/src/Reflection/MultiSizeTest2.v
@@ -168,7 +168,9 @@ Definition bound_op
(bound_type T2 (snd args2)))))
(Pair (Op (Cast _ _) (Var (fst args)))
(Op (Cast _ _) (Var (snd args))))))
- | Const _ _ as e, _
+ | Const _ _ as e, Plus _
+ | Const _ _ as e, Const _ _
+ | Const _ _ as e, Cast _ _
=> fun args args2 => Op e TT
| Cast _ _ as e, Plus _
| Cast _ _ as e, Const _ _