diff options
| author |  coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-02 12:02:14 +0000 |
|---|---|---|
| committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-02 12:02:14 +0000 |
| commit | 8b5128c023b7217058d2f3854fc1d4ab22dd8b4b (patch) | |
| tree | 34dd224c14814234d9fecfb16dce84b740f4ef44 /test-suite/success/TestRefine.v | |
| parent | 2292dd89b9b36ec8c865ab67e5291088bfcc4806 (diff) | |
Correction du bug 808: il est maintenant interdit de déclarer une assomption en cours de preuve.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8109 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/TestRefine.v')
| -rw-r--r-- | test-suite/success/TestRefine.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v index 8ed0f7ba6..82c5cf2e7 100644 --- a/test-suite/success/TestRefine.v +++ b/test-suite/success/TestRefine.v @@ -97,11 +97,10 @@ Abort. (************************************************************************) +Parameter f : nat * nat -> nat -> nat. Lemma essai : nat. -Parameter f : nat * nat -> nat -> nat. - refine (f _ ((fun x : nat => _:nat) 0)). Restart. |