Buenas,
nos esta pasando que en las maquinas de windows de la facultad este codigo es aceptado por el CoqIDE sin problemas:
Fixpoint length (A:Set)(l: list A) : nat :=
match l with
| nil => 0
| cons _ l' => S (length A l')
end.
Pero en las maquinas personales nos larga el siguiente error:
The constructor nil (in type list) expects 1 argument.
Lo cual se soluciona con el siguiente cambio:
Fixpoint length (A:Set)(l: list A) : nat :=
match l with
| nil _ => 0
| cons _ _ l' => S (length A l')
end.
Saludos,
Miguel.