diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-01-22 10:52:18 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-01-22 12:05:10 +0100 |
commit | e91ae93106b6bd6d92ef53ac18b04654485a8106 (patch) | |
tree | 30bfa5ada3f09a639f78130b0d5518ff4f266abe /test-suite/bugs/closed/5322.v | |
parent | 6ff62ec78d5517ec5905041fa2e4926e15ff89f0 (diff) |
Fixing bugs in typing "match" (regressions #5322 and #5324 + bugs with let-ins).
A cleaning done in ade2363e35 (Dec 2015) was hinting at bugs in typing
a matching over a "catch-all" variable, when let-ins occur in the
arity. However ade2363e35 failed to understand what was the correct
fix, introducing instead the regressions mentioned in #5322 and #5324.
This fixes all of #5322 and #5324, as well as the handling of let-ins
in the arity.
Thanks to Jason for helping in diagnosing the problem.
Diffstat (limited to 'test-suite/bugs/closed/5322.v')
-rw-r--r-- | test-suite/bugs/closed/5322.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5322.v b/test-suite/bugs/closed/5322.v new file mode 100644 index 000000000..01aec8f29 --- /dev/null +++ b/test-suite/bugs/closed/5322.v @@ -0,0 +1,14 @@ +(* Regression in computing types of branches in "match" *) +Inductive flat_type := Unit | Prod (A B : flat_type). +Inductive exprf (op : flat_type -> flat_type -> Type) {var : Type} : flat_type +-> Type := +| Op {t1 tR} (opc : op t1 tR) (args : exprf op t1) : exprf op tR. +Inductive op : flat_type -> flat_type -> Type := a : op Unit Unit. +Arguments Op {_ _ _ _} _ _. +Definition bound_op {var} + {src2 dst2} + (opc2 : op src2 dst2) + : forall (args2 : exprf op (var:=var) src2), Op opc2 args2 = Op opc2 args2. + refine match opc2 return (forall args2, Op opc2 args2 = Op opc2 args2) with + | _ => _ + end. |