diff options
| author | Maxime Dénès | 2016-10-03 11:09:03 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-10-03 11:13:40 +0200 |
| commit | a35a3fd5cf59e262e814afd530ffdc35f085c01d (patch) | |
| tree | 87a13102f6145c238b0696313ceb722beff09f00 /test-suite | |
| parent | 24d5448c65ba05072a5ab4180c9be95670ce126d (diff) | |
| parent | 0746578040e738d079bcc3289857bb99983a7a22 (diff) | |
Merge remote-tracking branch 'github/pr/304' into v8.6
Was PR#304: fixing bug 4609
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/Injection.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v index 8745cf2fbd..da2183841d 100644 --- a/test-suite/success/Injection.v +++ b/test-suite/success/Injection.v @@ -135,6 +135,21 @@ intros * [= H]. exact H. Abort. +(* Test the Keep Proof Equalities option. *) +Set Keep Proof Equalities. +Unset Structural Injection. + +Inductive pbool : Prop := Pbool1 | Pbool2. + +Inductive pbool_shell : Set := Pbsc : pbool -> pbool_shell. + +Goal Pbsc Pbool1 = Pbsc Pbool2 -> True. +injection 1. +match goal with + |- Pbool1 = Pbool2 -> True => idtac | |- True => fail +end. +Abort. + (* Injection does not project at positions in Prop... allow it? Inductive t (A:Prop) : Set := c : A -> t A. |