diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-12 20:10:52 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-12 20:10:52 +0000 |
| commit | b431b2c4955bf908de6976917dbdc7771596e940 (patch) | |
| tree | 56b9c0e34409815fbf57e0c96e2d0f8c3db2177f /test-suite/success/refine.v | |
| parent | bd66312570343037206be512285c1f10371d3a65 (diff) | |
Ajout exemple Yves
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5091 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/refine.v')
| -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 1eb84a9be..ad4eed5ae 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. |