aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-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 _ _