diff options
| -rw-r--r-- | test-suite/success/refine.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v index 1eb84a9bef..ad4eed5ae5 100644 --- a/test-suite/success/refine.v +++ b/test-suite/success/refine.v @@ -16,3 +16,15 @@ Refine let y = O in (plus O ?). Exact (S O). Save test3. +(* Example submitted by Yves on coqdev *) + +Require PolyList. + +Goal (l:(list nat))l=l. +Proof. +Refine [l]<[l]l=l> + Cases l of + | nil => ? + | (cons O l0) => ? + | (cons (S _) l0) => ? + end. |