Skip to content


Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Coq Repository at Nijmegen
Coq Other
branch: master

This branch is 119 commits ahead of robbertkrebbers:master

Merge pull request #14 from aa755/PullReq

3 lemmas. 1) intervals are convex 2) Min is contained in any interval containing the 2 args 3) same for max
latest commit f5d98c78ce
@spitters spitters authored
Failed to load latest commit information.
broken Moved ODE solver files to ode/
classes Replaced meet/join by their unicode notation ⊔ / ⊓
complex Pfew, resolved all names, s/Zero/[0]/ and s/One/[1]/
coq_reals Now compiles with Coq 8.4
doc Removing html files here, as they are now on:
dump Plot pgm s works again
examples Small changes in example
fta Pfew, resolved all names, s/Zero/[0]/ and s/One/[1]/
logic Make compile with recent version of math-classes.
metric2 Compiled lemmas moved to other parts of CoRN
metrics Pfew, resolved all names, s/Zero/[0]/ and s/One/[1]/
model Started proving that the function to which Picard operator is applied…
ode Now works ith 8.4pl4
old Required old file added back
order CoRN no longer depends on Ssreflect.
raster CoRN no longer depends on Ssreflect.
reals Update CSumsReals.v
site_scons/site_tools Merge math-classes, and make joint compilation work.
stdlib_omissions Moved some lemmas to other parts of CoRN
tactics not used anymore
tools Merge branch 'master' of /home/robbert/formath/math-classes
transc Make compile with 8.4 beta.
util Make compile with 8.4 beta.
.gitignore Merge pull request #5 from clarus/master
LICENSE Merge with Nijmegen: The configure generate Make using find
README Updating the math-classes submodule
SConstruct SConstruct is back The configure generate Make using find
description Updating description


C-CoRN, the Coq Constructive Repository at Nijmegen


This version of C-CoRN is known to compile with:

 - Coq 8.4pl4

 - SCons 1.2


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. 
Math Classes is contained in the C-CoRN git repository as a submodule. You can 
obtain math-classes automatically by giving the --recursive option when you 
clone the git repository:

  git clone --recursive

If you have already cloned the CoRN repository without --recursive, you can
still get the submodules with

  git submodule update --init --recursive


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 at


To build CoqDoc documentation, say "scons coqdoc".
Something went wrong with that request. Please try again.