The Coq mailing list

[Cuihtlauac ALVARADO <cuihtlauac.alvarado AT rd.francetelecom.fr>]

Hi all,

Ok, we suppose it comes from the new native "let in"
construct. Unfortunately, 6.x style could be far more readable,
sometimes.

Require PolyList.

Inductive foo : Set := bar : (list foo)->foo.

(* 6.3 : ok; 7.0 : error *)
Fixpoint interp [x:foo] : nat :=
let f = [l](fold_right plus O (map interp l)) in
Cases x of
| (bar l) => (f l)
end.

(* 6.3 : ok, 7.0 : ok *)
Fixpoint interp [x:foo] : nat :=
Cases x of
| (bar l) => (fold_right plus O (map interp l))
end.

Ciao

-- 
Cuihtlauac ALVARADO - France Telecom R & D - DTL/MSV/MFL
2, avenue Pierre Marzin - 22307 Lannion Cedex - France
Tel: +33 2 96 05 32 73 - Mob: +33 6 08 10 80 41 - Fax: +33 2 96 05 39 45