Rechercher

[CP16] Company-Coq: Taking Proof General one step closer to a real IDE

Conférences Internationales sans actes : CoqPL'16: International Workshop on Coq for Programming Languages, St Petersburgh, United-States, Florida,

Auteurs: P. Courtieu , C. Pit-Claudel

Mots clés: Interface, proof assistant

Résumé: We present the last development for coq around the emacs mode dedicated to proof assistant ProofGeneral and its company-cod mode. This mode is widely used among coq users.

Commentaires: Workshop satellite of POPL.

BibTeX

@conference {
CP16,
title="{Company-Coq: Taking Proof General one step closer to a real IDE}",
author=" P. Courtieu and C. Pit-Claudel ",
year=2016,
note="{Workshop satellite of POPL.}",
}