diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /test-suite/success/Case19.v | |
parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) |
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'test-suite/success/Case19.v')
-rw-r--r-- | test-suite/success/Case19.v | 21 |
1 files changed, 20 insertions, 1 deletions
diff --git a/test-suite/success/Case19.v b/test-suite/success/Case19.v index c29e5297..ce98879a 100644 --- a/test-suite/success/Case19.v +++ b/test-suite/success/Case19.v @@ -1,5 +1,5 @@ (* This used to fail in Coq version 8.1 beta due to a non variable - universe (issued by the inductive sort-polymorphism) being sent by + universe (issued by template polymorphism) being sent by pretyping to the kernel (bug #1182) *) Variable T : Type. @@ -17,3 +17,22 @@ Fail exists (fun x => with | eq_refl => eq_refl end). +Abort. + +(* Some tests with ltac matching on building "if" and "let" *) + +Goal forall b c d, (if negb b then c else d) = 0. +intros. +match goal with +|- (if ?b then ?c else ?d) = 0 => transitivity (if b then d else c) +end. +Abort. + +Definition swap {A} {B} '((x,y):A*B) := (y,x). + +Goal forall p, (let '(x,y) := swap p in x + y) = 0. +intros. +match goal with +|- (let '(x,y) := ?p in x + y) = 0 => transitivity (let (x,y) := p in x+y) +end. +Abort. |