diff options
-rw-r--r-- | pretyping/detyping.ml | 12 | ||||
-rwxr-xr-x | test-suite/check | 13 | ||||
-rw-r--r-- | test-suite/success/PPFix.v8 | 8 |
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. |