Coq with native compilation, as well as machine integers and arrays !
Switch branches/tags
Nothing to show
Clone or download
Permalink
Failed to load latest commit information.
checker lib directory is cut in 2 cma. Apr 25, 2012
config ./configure & freedesktop Dec 23, 2011
dev Towards 63-bits integers (working only on amd64 for now) Jul 16, 2013
doc Renamed Int31 to Int63. Jan 3, 2014
ide Fix coqide compilation with lablgtk 2.16 Dec 13, 2012
interp Towards 63-bits integers (working only on amd64 for now) Jul 16, 2013
kernel conversion of erroneous int32/int64 to int32_t/int64_t Nov 21, 2017
lib Bigint : better ensure canonicity of arrays of int blocks Jun 12, 2014
library Updated the interface between native_compute and the OCaml compiler. Sep 1, 2015
man Coqtop and coqc: cleaning description of options in RefMan and manpages. Jan 27, 2012
parsing Updated the interface between native_compute and the OCaml compiler. Sep 1, 2015
plugins Fix extraction of Uint63. May 28, 2014
pretyping Compiles with OCaml 4.05.0 Nov 13, 2017
proofs add tactic native_cast_no_check Jul 19, 2014
scripts Fix compilation in my setup. Dec 1, 2017
states merge with trunk 13523 Oct 12, 2010
tactics add tactic native_cast_no_check Jul 19, 2014
test-suite Fix mulc in VM. Jul 21, 2014
theories Renamed Int31 to Int63. Jan 3, 2014
tools Improve the coq_makefile tool so it is more robust w.r.t option "-I ." Jun 12, 2014
toplevel Compiles with OCaml 4.05.0 Nov 13, 2017
.dir-locals.el .dir-locals.el: Restrict the scope of eval to tuareg-mode buffers. Jun 12, 2014
.gitignore some #include <stdint.h> were missing Nov 21, 2017
CHANGES Remove the Dp plugin. Apr 26, 2012
COMPATIBILITY Credits for 8.4 + resetting COMPATIBILITY file. Dec 23, 2011
COPYRIGHT Version number, copyright, credits: missing updates. Jan 27, 2012
CREDITS Version number, copyright, credits: missing updates. Jan 27, 2012
INSTALL - changing minimal version for OCaml: Coq uses Filename.dirsep that i… Feb 22, 2012
INSTALL.doc git-svn-id: svn://scm.gforge.inria.fr/svn/coq/branches/native@13228 8… Jul 1, 2010
INSTALL.ide CoqIdE configuration file won't pollute your home anymore Dec 23, 2011
INSTALL.macosx git-svn-id: svn://scm.gforge.inria.fr/svn/coq/branches/native@13228 8… Jul 1, 2010
LICENSE git-svn-id: svn://scm.gforge.inria.fr/svn/coq/branches/native@13228 8… Jul 1, 2010
Makefile Makefile: clean target now removes compiled libraries cmxs. Jul 28, 2012
Makefile.build parsing/grammar.cma must be linked with unix.cma Dec 7, 2015
Makefile.common Including native compiler .o files in install target. Jan 11, 2013
Makefile.doc Improved synchronisation of stdlib index page with current library st… Feb 22, 2012
README - changing minimal version for OCaml: Coq uses Filename.dirsep that i… Feb 22, 2012
README.doc git-svn-id: svn://scm.gforge.inria.fr/svn/coq/branches/native@13228 8… Jul 1, 2010
README.win Win32: remove the need for Coq.bat and Coqide.bat May 5, 2011
TODO git-svn-id: svn://scm.gforge.inria.fr/svn/coq/branches/native@13228 8… Jul 1, 2010
_tags lib directory is cut in 2 cma. Apr 25, 2012
build lib directory is cut in 2 cma. Apr 25, 2012
configure Patch to compile with Make 4. Jan 2, 2014
coq-win32.itarget git-svn-id: svn://scm.gforge.inria.fr/svn/coq/branches/native@13228 8… Jul 1, 2010
coq.itarget git-svn-id: svn://scm.gforge.inria.fr/svn/coq/branches/native@13228 8… Jul 1, 2010
install.sh git-svn-id: svn://scm.gforge.inria.fr/svn/coq/branches/native@13228 8… Jul 1, 2010
myocamlbuild.ml lib directory is cut in 2 cma. Apr 25, 2012

README

               	         THE COQ V8 SYSTEM
            	         =================

INSTALLATION.
=============

   See the file INSTALL for installation procedure.


DOCUMENTATION.
==============

   The documentation is part of the archive in directory doc. The
   documentation of the last released version is available on the Coq
   web site at http://coq.inria.fr/doc.


CHANGES.
========

   There is a file named CHANGES that explains the differences and the
   incompatibilities since last versions. If you upgrade Coq, please read
   it carefully.


AVAILABILITY.
=============

   Coq is available at http://coq.inria.fr, or, for older versions at
   ftp://ftp.inria.fr/INRIA/LogiCal/coq.


THE COQ CLUB.
=============

   The Coq Club moderated mailing list is meant to be a standard way to
   discuss questions about the Coq system and related topics. The submission
   address is:

	coq-club@inria.fr

   The topics to be discussed in the club should include:

     * technical problems;

     * questions about proof developments;

     * suggestions and questions about the implementation;

     * announcements of proofs;

     * theoretical questions about typed lambda-calculi which are
       closely related to Coq.

   To be added to, or removed from, the mailing list, please write to:

	coq-club-request@inria.fr

   Please use also this address for any questions/suggestions about the
   Coq Club. It might sometimes take a few days before your messages get
   forwarded.


BUGS REPORT.
============

   Send your bug reports by filling a form at

        http://coq.inria.fr/bugs

   To be effective, bug reports should mention the Caml version used
   to compile and run Coq, the Coq version (coqtop -v), the configuration
   used, and include a complete source example leading to the bug.