The Coq mailing list

[Olivier PONS <Olivier.Pons AT sophia.inria.fr>]

Bonjour,

Ya t'il un moyen simple de lancer Coq (et coqc) sans que tout les fichiers de 
INIT soient charges.
En fait je voudrait pouvoir charger une version modifiee de Peano sans 
qu'elle interfere avec celle qui se trouve dans INIT.


Pour l'instant si je redefini un Theoreme (d'ailleur pourquoi il n'y a pas de 
clash? ) la preuve que j'obtient n'est pas la meme et utilise la version 
precedent la redefinition.

Exemple sur n_Sn defini dans Peano.


Coq < Print  n_Sn.
n_Sn = 
[n:nat]
 (nat_ind [n0:nat]~n0=(S n0) (O_S O)
   [n0:nat][H:~n0=(S n0)](not_eq_S n0 (S n0) H) n)
     : (n:nat)~n=(S n)

(* je le redeffini *) 
Theorem n_Sn : (n:nat) ~(n=(S n)).
 Induction n ; Auto.
Qed.

Coq < Print  n_Sn.                      
n_Sn = 
[n:nat]
 (nat_ind [n0:nat]~n0=(S n0) (O_S O)
   [n0:nat][_:~n0=(S n0)](n_Sn.cci (S n0)) n)
     : (n:nat)~n=(S n)


Olivier