diff options
Diffstat (limited to 'test-suite/bugs')
-rw-r--r-- | test-suite/bugs/closed/2800.v | 13 | ||||
-rw-r--r-- | test-suite/bugs/closed/5500.v | 35 | ||||
-rw-r--r-- | test-suite/bugs/closed/5547.v | 16 | ||||
-rw-r--r-- | test-suite/bugs/closed/7700.v | 9 | ||||
-rw-r--r-- | test-suite/bugs/closed/7779.v | 15 | ||||
-rw-r--r-- | test-suite/bugs/closed/7780.v | 16 |
6 files changed, 104 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/2800.v b/test-suite/bugs/closed/2800.v index 2ee438934..54c75e344 100644 --- a/test-suite/bugs/closed/2800.v +++ b/test-suite/bugs/closed/2800.v @@ -4,3 +4,16 @@ intuition match goal with | |- _ => idtac " foo" end. + + lazymatch goal with _ => idtac end. + match goal with _ => idtac end. + unshelve lazymatch goal with _ => idtac end. + unshelve match goal with _ => idtac end. + unshelve (let x := I in idtac). +Abort. + +Require Import ssreflect. + +Goal True. +match goal with _ => idtac end => //. +Qed. diff --git a/test-suite/bugs/closed/5500.v b/test-suite/bugs/closed/5500.v new file mode 100644 index 000000000..aa63e2ab0 --- /dev/null +++ b/test-suite/bugs/closed/5500.v @@ -0,0 +1,35 @@ +(* Too weak check on the correctness of return clause was leading to an anomaly *) + +Inductive Vector A: nat -> Type := + nil: Vector A O +| cons: forall n, A -> Vector A n -> Vector A (S n). + +(* This could be made working with a better inference of inner return + predicates from the return predicate at the higher level of the + nested matching. Currently, we only check that it does not raise an + anomaly, but eventually, the "Fail" could be removed. *) + +Fail Definition hd_fst A x n (v: A * Vector A (S n)) := + match v as v0 return match v0 with + (l, r) => + match r in Vector _ n return match n with 0 => Type | S _ => Type end with + nil _ => A + | cons _ _ _ _ => A + end + end with + (_, nil _) => x + | (_, cons _ n hd tl) => hd + end. + +(* This is another example of failure but involving beta-reduction and + not iota-reduction. Thus, for this one, I don't see how it could be + solved by small inversion, whatever smart is small inversion. *) + +Inductive A : (Type->Type) -> Type := J : A (fun x => x). + +Fail Check fun x : nat * A (fun x => x) => + match x return match x with + (y,z) => match z in A f return f Type with J => bool end + end with + (y,J) => true + end. diff --git a/test-suite/bugs/closed/5547.v b/test-suite/bugs/closed/5547.v new file mode 100644 index 000000000..79633f489 --- /dev/null +++ b/test-suite/bugs/closed/5547.v @@ -0,0 +1,16 @@ +(* Checking typability of intermediate return predicates in nested pattern-matching *) + +Inductive A : (Type->Type) -> Type := J : A (fun x => x). +Definition ret (x : nat * A (fun x => x)) + := match x return Type with + | (y,z) => match z in A f return f Type with + | J => bool + end + end. +Definition foo : forall x, ret x. +Proof. +Fail refine (fun x + => match x return ret x with + | (y,J) => true + end + ). diff --git a/test-suite/bugs/closed/7700.v b/test-suite/bugs/closed/7700.v new file mode 100644 index 000000000..56f5481ba --- /dev/null +++ b/test-suite/bugs/closed/7700.v @@ -0,0 +1,9 @@ +(* Abbreviations to section variables were not located *) +Section foo. + Let x := Set. + Notation y := x. + Check y. + Variable x' : Set. + Notation y' := x'. + Check y'. +End foo. diff --git a/test-suite/bugs/closed/7779.v b/test-suite/bugs/closed/7779.v new file mode 100644 index 000000000..78936b595 --- /dev/null +++ b/test-suite/bugs/closed/7779.v @@ -0,0 +1,15 @@ +(* Checking that the "in" clause takes the "eqn" clause into account *) + +Definition test (x: nat): {y: nat | False }. Admitted. + +Parameter x: nat. +Parameter z: nat. + +Goal + proj1_sig (test x) = z -> + False. +Proof. + intro H. + destruct (test x) eqn:Heqs in H. + change (test x = exist (fun _ : nat => False) x0 f) in Heqs. (* Check it has the expected statement *) +Abort. diff --git a/test-suite/bugs/closed/7780.v b/test-suite/bugs/closed/7780.v new file mode 100644 index 000000000..2318f4d6e --- /dev/null +++ b/test-suite/bugs/closed/7780.v @@ -0,0 +1,16 @@ +(* A lift was missing in expanding aliases under binders for unification *) + +(* Below, the lift was missing while expanding the reference to + [mkcons] in [?N] which was under binder [arg] *) + +Goal forall T (t : T) (P P0 : T -> Set), option (option (list (P0 t)) -> option (list (P t))). + intros ????. + refine (Some + (fun rls + => let mkcons := ?[M] in + let default arg := ?[N] in + match rls as rls (* 2 *) return option (list (P ?[O])) with + | Some _ => None + | None => None + end)). +Abort. |