proof assistant for higher-order logic (gtk interface)
Coq is a proof assistant for higher-order logic, which allows the
development of computer programs consistent with their formal
specification. It is developed using Objective Caml and Camlp5.
This package provides CoqIde, a graphical user interface for
coq (8.2~rc2+dfsg-1) experimental; urgency=low
The Coq library for programming in OCaml is now in its own binary
package, libcoq-ocaml-dev, along with coqmktop. The theories have been
moved from coq-libs to the more expressive name coq-theories.
-- Stéphane Glondu <email@example.com> Mon, 02 Feb 2009 09:48:03 +0100
Q0) What is CoqIde?
R0: A powerfull graphical interface for Coq. See http://coq.inria.fr. for more informations.
Q1) How to enable Emacs keybindings?
gtk-key-theme-name = "Emacs"
in your ".coqide-gtk2rc" file. It may be in the current dir
or in $HOME dir. This is done by default.
Q2) How to enable antialiased fonts?
R2) Set the GDK_USE_XFT variable to 1. This
coqide - The Coq Proof Assistant graphical interface
coqide [ options ]
coqtop is a gtk graphical interface for the Coq proof assis‐
For command-line-oriented use of Coq, see coqide(1) ; for
batch-oriented use of Coq, see coqc(1).
coq (8.2.pl2+dfsg-1) unstable; urgency=low
* New upstream release
- compiles with OCaml 3.12
Changes from V8.2 to forthcoming V8.2pl1
Language and comm
This package was debianized by Fernando Sanchez <firstname.lastname@example.org>
It was downloaded from
Browse inside coqide_8.2.pl2+dfsg-1_amd64.deb
Results 1 - 1 of 1Search over 15 billion files
© 1997-2017 FileWatcher.com