J'utilise CoqIDE pour compléter les exercices dans le livre Software Foundations sur Coq. Je peux compiler avec succès Basics.v, résultant dans Basics.vo et Basics.glob dans mon répertoire. Lorsque j'essaie d'exécuter Induction.v, cela fonctionne. Lorsque j'essaie de le compiler, il se plaint de tonnes de références manquantes, telles que evenb et negb_involutive. Si je copie le contenu de Basics.v dans Induction.v, il compile, mais évidemment, ce n'est pas le chemin à parcourir.La référence "X" n'a pas été trouvée dans l'environnement actuel
Ce n'est pas une copie de la question Coq error: The reference evenb was not found in the current environment, comme je l'ai déjà fait ces choses:
Compile Basics.v. Vérifiez si Basics.vo est dans le répertoire. Maintenant, compilez Induction.v. Cette dernière étape échoue.
Je l'ai essayé tout à l'heure (j'ai téléchargé une nouvelle copie de SF et compilé depuis le menu à l'intérieur de CoqIDE) et je n'ai eu aucune erreur. Pourriez-vous expliquer un peu plus ce que vous faites? Quelle version de Coq avez-vous? J'ai 8.5pl2. – larsr
J'ai tout résolu à l'intérieur de Basics.v et Induction.v. J'ai la même version que toi. Peut-être devrais-je essayer de compiler les versions "vides" à la place. Je rapporterai. – RaptorDotCpp
@larsr J'ai aussi téléchargé la nouvelle copie. J'ai ouvert CoqIDE, ouvert Basics.v, puis l'ai compilé. C'était réussi. Quand j'ai alors ouvert Induction.v et essayé de le compiler, j'ai eu la même erreur qu'avant. Donc, même la nouvelle copie ne semble pas compiler sur mon système. J'utilise Mac OS X El Capitan. – RaptorDotCpp