bug de PP des fix (coqbugs #574)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5550 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 28 insertions, 5 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index d8c97bddd..67cf0d388 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -390,6 +390,7 @@ and share_names tenv n l avoid env c t =
     (List.rev l,c,t)
   else
   match kind_of_term c, kind_of_term t with
+    (* factorize even when not necessary to have better presentation *)
     | Lambda (na,t,c), Prod (na',t',c') ->
         let na = match (na,na') with
             Name _, _ -> na
@@ -400,21 +401,22 @@ and share_names tenv n l avoid env c t =
         let avoid = id::avoid and env = add_name (Name id) env in
         share_names tenv (n-1) ((Name id,None,t)::l) avoid env c c'
     (* May occur for fix built interactively *)
-    | LetIn (na,b,t',c), _ ->
+    | LetIn (na,b,t',c), _ when n > 0 ->
         let t' = detype tenv avoid env t' in
         let b = detype tenv avoid env b in
 	let id = next_name_away na avoid in 
         let avoid = id::avoid and env = add_name (Name id) env in
         share_names tenv n ((Name id,Some b,t')::l) avoid env c t
     (* Only if built with the f/n notation or w/o let-expansion in types *)
-    | _, LetIn (_,b,_,t) ->
+    | _, LetIn (_,b,_,t) when n > 0 ->
 	share_names tenv n l avoid env c (subst1 b t)
     (* If it is an open proof: we cheat and eta-expand *)
-    | _, Prod (na',t',c') ->
+    | _, Prod (na',t',c') when n > 0 ->
         let t' = detype tenv avoid env t' in
-        let avoid = name_cons na' avoid and env = add_name na' env in
+	let id = next_name_away na' avoid in 
+        let avoid = id::avoid and env = add_name (Name id) env in
         let appc = mkApp (lift 1 c,[|mkRel 1|]) in
-        share_names tenv (n-1) ((na',None,t')::l) avoid env appc c'
+        share_names tenv (n-1) ((Name id,None,t')::l) avoid env appc c'
     (* If built with the f/n notation: we renounce to share names *)
     | _ ->
         if n>0 then warning "Detyping.detype: cannot factorize fix enough";
diff --git a/test-suite/check b/test-suite/check
index 65c4197eb..1c7822d10 100755
--- a/test-suite/check
+++ b/test-suite/check
@@ -39,6 +39,19 @@ test_success() {
 	    echo "V7 Error! (should be accepted)"
         fi 
     done
+    for f in $1/*.v8; do 
+	nbtests=`expr $nbtests + 1`
+	printf "    "$f"..."
+        cp $f tmp8.v
+	$command tmp8.v > /dev/null 2>&1
+        if [ $? = 0 ]; then
+            echo "Ok"
+            nbtestsok=`expr $nbtestsok + 1`
+        else
+            echo "V8 Error! (should be accepted)"
+        fi
+        rm tmp8.v
+    done
 }
 
 # La fonction suivante teste le compilateur sur des fichiers qu'il doit
diff --git a/test-suite/success/PPFix.v8 b/test-suite/success/PPFix.v8
new file mode 100644
index 000000000..1ecbae3ab
--- /dev/null
+++ b/test-suite/success/PPFix.v8
@@ -0,0 +1,8 @@
+
+(* To test PP of fixpoints *)
+Require Import Arith.
+Check fix a(n: nat): n<5 -> nat :=
+  match n return n<5 -> nat with
+    | 0 => fun _ => 0
+    | S n => fun h => S (a n (lt_S_n _ _ (lt_S _ _ h)))
+  end.