diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-04-08 18:36:36 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:59:00 +0200 |
| commit | bfbef3d5e9d1262e29ce5ed68acf6f33de603f39 (patch) | |
| tree | 1945def6d446848997a7e18c068d4cb5c3e36902 | |
| parent | b6cf2215494165d3d1089881b3566ad8a153f33a (diff) | |
Comment in Funind.v test-suite file
| -rw-r--r-- | test-suite/success/Funind.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v index 1ed2221cc..dcf7b249a 100644 --- a/test-suite/success/Funind.v +++ b/test-suite/success/Funind.v @@ -23,7 +23,7 @@ Function ftest (n m : nat) : nat := end | S p => 0 end. -(* MS: FIXME: apparently can't define R_ftest_complete *) +(* MS: FIXME: apparently can't define R_ftest_complete. Rest of the file goes through. *) Lemma test1 : forall n m : nat, ftest n m <= 2. intros n m. |