diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/InversionSigma.v | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/test-suite/success/InversionSigma.v b/test-suite/success/InversionSigma.v index c19939eabe..51f33c7ce7 100644 --- a/test-suite/success/InversionSigma.v +++ b/test-suite/success/InversionSigma.v @@ -1,6 +1,6 @@ Section inversion_sigma. Local Unset Implicit Arguments. - Context A (B : A -> Prop) (C : forall a, B a -> Prop) + Context A (B : A -> Prop) (C C' : forall a, B a -> Prop) (D : forall a b, C a b -> Prop) (E : forall a b c, D a b c -> Prop). (* Require that, after destructing sigma types and inverting @@ -11,6 +11,8 @@ Section inversion_sigma. repeat match goal with | [ H : sig _ |- _ ] => destruct H | [ H : sigT _ |- _ ] => destruct H + | [ H : sig2 _ _ |- _ ] => destruct H + | [ H : sigT2 _ _ |- _ ] => destruct H end; simpl in *; inversion_sigma; repeat match goal with @@ -27,4 +29,12 @@ Section inversion_sigma. Goal forall (x y : { a : A | { b : { b : B a | C a b } | { d : D a (proj1_sig b) (proj2_sig b) | E _ _ _ d } } }) (p : x = y), p = p. Proof. test_inversion_sigma. Qed. + + Goal forall (x y : { a : { a : A & B a } & C _ (projT2 a) & C' _ (projT2 a) }) + (p : x = y), p = p. + Proof. test_inversion_sigma. Qed. + + Goal forall (x y : { a : { a : A & B a } | C _ (projT2 a) & C' _ (projT2 a) }) + (p : x = y), p = p. + Proof. test_inversion_sigma. Qed. End inversion_sigma. |