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