diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-18 19:38:19 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-25 10:59:24 +0100 |
| commit | df9d69f3ccf3e5600919a21112afda00b463fbc5 (patch) | |
| tree | 95bcb0f7e45ae7c6f3e9c1584f2551862ee947f2 /test-suite/success | |
| parent | c3e01a044297d322d8a5e6830fe3af002ebd2dce (diff) | |
Fixing a bug in the order of side conditions for introduction pattern -> and <-.
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/intros.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index 11156aa0e..69d66f100 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -84,3 +84,17 @@ Qed. Goal forall x : nat, True. intros y%(fun x => x). Abort. + +(* Fixing a bug in the order of side conditions of a "->" step *) + +Goal (True -> 1=0) -> 1=1. +intros ->. +- reflexivity. +- exact I. +Qed. + +Goal forall x, (True -> x=0) -> 0=x. +intros x ->. +- reflexivity. +- exact I. +Qed. |