diff options
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. |