From c078cba1208255cd2a2f5b60b6d10cb85b6e9cb2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 6 Dec 2004 14:03:53 +0000
Subject: Ajout bug #888

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6417 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/refine.v | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v
index acd9cf1421..bc81462bf2 100644
--- a/test-suite/success/refine.v
+++ b/test-suite/success/refine.v
@@ -30,10 +30,26 @@ Refine [l]<[l]l=l>
        end.
 Abort.
 
+(* Submitted by Roland Zumkeller (bug #888) *)
+
+(* The Fix and CoFix rules expect a subgoal even for closed components of the
+   (co-)fixpoint *)
+
+Goal nat -> nat.
+Refine(
+  Fix f {f [n:nat] : nat := (S ?) with
+         pred [n:nat] : nat := n}).
+Intro; Exact 0.
+Qed.
+
 (* Submitted by Roland Zumkeller (bug #889) *)
 
+(* The types of metas were in metamap and they were not updated when
+   passing through a binder *)
+
 Goal (n:nat) nat -> n=0.
 Refine [n]
   Fix f { f [i:nat] : n=0 :=
     Cases i of 0 => ? | (S _) => ? end }.
 Abort.
+
-- 
cgit v1.2.3