The Coq mailing list

[Jakubiec Line <jakubiec AT lif.univ-mrs.fr>]

 Bonjour,

J'utilise depuis peu la version V8 de Coq sous Linux (version rpm)
et j'ai des problèmes à la compilation:

$ coq_makefile Fic.v > Makefile
Fatal error: the file Fic.v is not a bytecode executable file

Pour le test, Fic.v contient seulement le code source suivant:
--
Require Export Bool.

Lemma bool_dec : forall b:bool, {b=true}+{b=false}.
induction b; auto.
Save.
Hint Immediate bool_dec.

Lemma orb_sym : forall a b:bool, (orb a b)=(orb b a).
induction a; induction b; auto.
Save.
Hint Immediate orb_sym.
--

Avec coqc, j'ai la même erreur.

Merci pour votre aide.

     Line

--
(**************************************************************************)
(* Line Jakubiec - Laboratoire d'Informatique Fondamentale de Marseille   *)
(* Université de la Méditerranée (Aix-Marseille II)                       *)
(* Faculté des Sciences de Luminy                                         *)
(* 163, Avenue de Luminy                                                  *)
(* 13288 - MARSEILLE Cedex 9                                              *)
(**************************************************************************)