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/success/Case22.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/success/Case22.v')
-rw-r--r-- | test-suite/success/Case22.v | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v index 3c696502c..465b3eb8c 100644 --- a/test-suite/success/Case22.v +++ b/test-suite/success/Case22.v @@ -41,6 +41,7 @@ Definition F (x:IND True) (A:Type) := Theorem paradox : False. (* This succeeded in 8.3, 8.4 and 8.5beta1 because F had wrong type *) Fail Proof (F C False). +Abort. (* Another bug found in November 2015 (a substitution was wrongly reversed at pretyping level) *) @@ -61,3 +62,30 @@ Inductive Ind2 (b:=1) (c:nat) : Type := Constr2 : Ind2 c. Eval vm_compute in Constr2 2. + +(* A bug introduced in ade2363 (similar to #5322 and #5324). This + commit started to see that some List.rev was wrong in the "var" + case of a pattern-matching problem but it failed to see that a + transformation from a list of arguments into a substitution was + still needed. *) + +(* The order of real arguments was made wrong by ade2363 in the "var" + case of the compilation of "match" *) + +Inductive IND2 : forall X Y:Type, Type := + CONSTR2 : IND2 unit Empty_set. + +Check fun x:IND2 bool nat => + match x in IND2 a b return a with + | y => _ + end = true. + +(* From January 2017, using the proper function to turn arguments into + a substitution up to a context possibly containing let-ins, so that + the following, which was wrong also before ade2363, now works + correctly *) + +Check fun x:Ind bool nat => + match x in Ind _ X Y Z return Z with + | y => (true,0) + end. |