diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-05 18:18:22 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-05 18:18:22 +0200 |
| commit | 2dcd8f2e82366bb3b0f51a42426ccdfbb00281dc (patch) | |
| tree | 4e9a44599dec13e262538e70a6a60bcf3e5fa97e /test-suite/success/Injection.v | |
| parent | 01a448be0133872a686e613ab1034b4cb97cd666 (diff) | |
| parent | 8114da3ba8a9b31ffe194e7f7f0239ecc2219b9c (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'test-suite/success/Injection.v')
| -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 8745cf2fb..da2183841 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. |