diff options
| -rw-r--r-- | test-suite/success/refine.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v index bc81462bf2..47453b9ca7 100644 --- a/test-suite/success/refine.v +++ b/test-suite/success/refine.v @@ -39,7 +39,7 @@ Goal nat -> nat. Refine( Fix f {f [n:nat] : nat := (S ?) with pred [n:nat] : nat := n}). -Intro; Exact 0. +Exact 0. Qed. (* Submitted by Roland Zumkeller (bug #889) *) |