diff options
| author | Hugo Herbelin | 2015-12-18 08:23:35 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-25 10:59:24 +0100 |
| commit | c3e01a044297d322d8a5e6830fe3af002ebd2dce (patch) | |
| tree | 8520413956cbfb57e26979dd4201ec7619b74fc2 /test-suite/success/Injection.v | |
| parent | 1f2cc4026cd5e977979ff1507fd5fa0d96e1a92f (diff) | |
Fixing an "injection as" bug in the presence of side conditions.
Diffstat (limited to 'test-suite/success/Injection.v')
| -rw-r--r-- | test-suite/success/Injection.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v index 25e464d677..8fd0394625 100644 --- a/test-suite/success/Injection.v +++ b/test-suite/success/Injection.v @@ -68,6 +68,12 @@ einjection (H O). instantiate (1:=O). Abort. +Goal (forall x y : nat, x = y -> S x = S y) -> True. +intros. +einjection (H O) as H0. +instantiate (y:=O). +Abort. + (* Test the injection intropattern *) Goal forall (a b:nat) l l', cons a l = cons b l' -> a=b. |