diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
tree | 074182834cb406d1304aec4233718564a9c06ba1 /test-suite/success/specialize.v | |
parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) |
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'test-suite/success/specialize.v')
-rw-r--r-- | test-suite/success/specialize.v | 20 |
1 files changed, 19 insertions, 1 deletions
diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v index c5f032be..3faa1ca4 100644 --- a/test-suite/success/specialize.v +++ b/test-suite/success/specialize.v @@ -45,4 +45,22 @@ specialize eq_trans with _ a b c. intros _. (* Anomaly: Evar ?88 was not declared. Please report. *) *) -Abort.
\ No newline at end of file +Abort. + +(* Test use of pose proof and assert as a specialize *) + +Goal True -> (True -> 0=0) -> False -> 0=0. +intros H0 H H1. +pose proof (H I) as H. +(* Check that the hypothesis is in 2nd position by removing the top one *) +match goal with H:_ |- _ => clear H end. +match goal with H:_ |- _ => exact H end. +Qed. + +Goal True -> (True -> 0=0) -> False -> 0=0. +intros H0 H H1. +assert (H:=H I). +(* Check that the hypothesis is in 2nd position by removing the top one *) +match goal with H:_ |- _ => clear H end. +match goal with H:_ |- _ => exact H end. +Qed. |