WikiUFR Math-Info

Il faut installer à la fois coq et coqide (l'interface graphique pour coq).

Attention il se peut que les raccourcis par défaut dans coqide soient en conflit avec des raccourcis pour changer de session dans les terminaux X. Pour tester il faut lancer coqide et copier-coller :

 Lemma essai : forall A B,
 A /\ B -> B /\ A.
 Proof.
 intros.
 tauto.
 Qed.

Placer le curseur sur tauto et appuyer sur le raccourci qui apparait dans le menu “navigation” pour la commande “Go to” (ctrl-alt- flèche vers la droite à priori). Logiquement le texte jusqu'à tauto doit passer en vert.

Si il y a un changement de session X c'est qu'il y a un conflit avec les raccourcis de coqide.