Coq Repository at Nijmegen
Coq Other
Switch branches/tags
Nothing to show
Clone or download
spitters Merge pull request #54 from ppedrot/fix-52
Fix #52: `cofix` tactic without a name is deprecated.
Latest commit 4b91659 May 24, 2018
Permalink
Failed to load latest commit information.
algebra Change Implicit Arguments to Arguments in CoRN Feb 24, 2018
broken Updated proof of Liouville's theorem Dec 12, 2017
classes Absolutize all [Import]s Mar 1, 2016
complex Merge branch 'cornmaster' into allfixes Apr 19, 2016
coq_reals Make proofs oblivious to the changes in the definition of IZR. Mar 8, 2017
doc Removing html files here, as they are now on: Jun 2, 2014
dump Plot pgm s works again Mar 8, 2011
examples Fix obsolete vernacular syntax for locality. Nov 7, 2017
fta Change Implicit Arguments to Arguments in CoRN Feb 24, 2018
ftc Change Implicit Arguments to Arguments in CoRN Feb 24, 2018
liouville Removed the ssreflect dependency and fixed some "Admitted" Jan 8, 2018
logic Change Implicit Arguments to Arguments in CoRN Feb 24, 2018
metric2 Merge pull request #54 from ppedrot/fix-52 May 24, 2018
metrics Change Implicit Arguments to Arguments in CoRN Feb 24, 2018
model Change Implicit Arguments to Arguments in CoRN Feb 24, 2018
ode Change Implicit Arguments to Arguments in CoRN Feb 24, 2018
old Required old file added back Sep 25, 2014
order Change Implicit Arguments to Arguments in CoRN Feb 24, 2018
raster Fixing compilaton wrt. Coq 8.5 May 19, 2016
reals Merge pull request #54 from ppedrot/fix-52 May 24, 2018
site_scons/site_tools Merge math-classes, and make joint compilation work. Dec 1, 2010
stdlib_omissions Get rid of `'` to provide compatibility with coq/coq#6155 Mar 8, 2018
tactics Change Implicit Arguments to Arguments in CoRN Feb 24, 2018
tools Merge branch 'master' of /home/robbert/formath/math-classes May 26, 2011
transc crtrans.vo is compiling via scons. Apr 20, 2016
util Merge branch 'cornmaster' into allfixes Apr 19, 2016
.gitignore adding "Make" and "Makefile" Jun 6, 2016
.travis.yml Fixing Travis Nov 7, 2017
LICENSE Merge with Nijmegen: Sep 26, 2006
Make Updated proof of Liouville's theorem Dec 12, 2017
Make.in The configure generate Make using find Sep 25, 2014
Makefile Updated proof of Liouville's theorem Dec 12, 2017
README.md Update README.md Oct 27, 2017
SConstruct updated SConstruct for the new version of Liouville Dec 13, 2017
configure.sh Updated proof of Liouville's theorem Dec 12, 2017
description Updating description Apr 4, 2014

README.md

C-CoRN

The Coq Constructive Repository at Nijmegen.

Install with OPAM

Make sure that you added the Coq repository:

opam repo add coq-released https://coq.inria.fr/opam/released

and run:

opam install coq-corn

Install from source

Prerequisites

This version of C-CoRN should compile with 8.6 and later. It requires

  • SCons 1.2 or make

Git checkout and submodules

C-CoRN depends on Math Classes, which is a library of abstract interfaces for mathematical structures that is heavily based on Coq's new type classes.

Building C-CoRN

C-CoRN uses SCons for its build infrastructure. SCons is a modern Python-based Make-replacement.

To build C-CoRN with SCons say scons to build the whole library, or scons some/module.vo to just build some/module.vo (and its dependencies).

In addition to common Make options like -j N and -k, SCons supports some useful options of its own, such as --debug=time, which displays the time spent executing individual build commands.

scons -c replaces Make clean

For more information, see the SCons documentation. Make is still supported.

Building documentation

To build CoqDoc documentation, say scons coqdoc.