Merge branch 'cornmaster' into allfixes

.gitignore

@@ -1,3 +1,6 @@
+Make
+Makefile
+Makefile.bak
 *.vo
 *.d
 *.glob

Make.in

@@ -0,0 +1,4 @@
+# Library name
+-R . CoRN
+
+# Coq files

README.md

@@ -0,0 +1,40 @@
+# C-CoRN
+> The Coq Constructive Repository at Nijmegen.
+
+## Install with OPAM
+Make sure that you added the [Coq repository](http://coq.io/opam/):
+
+    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 is known to compile with:
+
+* Coq 8.4pl4
+* SCons 1.2 or make
+
+### Git checkout and submodules
+C-CoRN depends on [Math Classes](https://github.com/math-classes/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](http://www.scons.org/) 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](http://www.scons.org/). Make is still supported.
+
+### Building documentation
+To build CoqDoc documentation, say `scons coqdoc`.

SConstruct

@@ -21,21 +21,19 @@ while nodes:
     nodes += glob.glob(node + '/*')
 
 includes = ' '.join(map(lambda x: '-I ' + x, dirs[1:]))
-Rs = '-R . CoRN -R math-classes/src MathClasses'
+Rs = '-R . CoRN'
 coqcmd = 'coqc ${str(SOURCE)[:-2]} ' + Rs
 
 env['COQFLAGS'] = Rs
 
 for node in vs: env.Coq(node, COQCMD=coqcmd)
 
-mc_vs, mc_vos, mc_globs = env.SConscript(dirs='math-classes/src')
-
-os.system('coqdep ' + ' '.join(map(str, vs+mc_vs)) + ' ' + includes + ' ' + Rs + ' > deps')
+os.system('coqdep ' + ' '.join(map(str, vs)) + ' ' + includes + ' ' + Rs + ' > deps')
 ParseDepends('deps')
 
 open('coqidescript', 'w').write('#!/bin/sh\ncoqide ' + Rs + ' $@ \n')
 os.chmod('coqidescript', 0755)
 
-env.CoqDoc(env.Dir('coqdoc'), vs+mc_vs, COQDOCFLAGS='-utf8 --toc -g --no-lib-name --coqlib http://coq.inria.fr/library')
+env.CoqDoc(env.Dir('coqdoc'), vs, COQDOCFLAGS='-utf8 --toc -g --no-lib-name --coqlib http://coq.inria.fr/library')
 
-#env.Command('deps.dot', [], 'tools/DepsToDot.hs < deps > $TARGET')
+#env.Command('deps.dot', [], 'tools/DepsToDot.hs < deps > $TARGET')

algebra/Bernstein.v

@@ -19,13 +19,13 @@ IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
 CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
 *)
 
-Require Export CPolynomials.
-Require Import CSums.
-Require Import Rational.
-Require Import Qordfield.
-Require Import COrdFields2.
-Require Import CRing_Homomorphisms.
-Require Vector.
+Require Export CoRN.algebra.CPolynomials.
+Require Import CoRN.algebra.CSums.
+Require Import CoRN.tactics.Rational.
+Require Import CoRN.model.ordfields.Qordfield.
+Require Import CoRN.algebra.COrdFields2.
+Require Import CoRN.algebra.CRing_Homomorphisms.
+Require Coq.Vectors.Vector.
 Export Vector.VectorNotations.
 
 Set Implicit Arguments.

algebra/CAbGroups.v

@@ -33,7 +33,7 @@
  * with this work; if not, write to the Free Software Foundation, Inc.,
  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  *)
-Require Export CGroups.
+Require Export CoRN.algebra.CGroups.
 
 Section Abelian_Groups.
 

algebra/CAbMonoids.v

@@ -33,9 +33,9 @@
  * with this work; if not, write to the Free Software Foundation, Inc.,
  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  *)
-Require Export CMonoids.
+Require Export CoRN.algebra.CMonoids.
 
-Require Import SetoidPermutation Setoid Morphisms.
+Require Import CoRN.util.SetoidPermutation Coq.Setoids.Setoid Coq.Classes.Morphisms.
 
 Section Abelian_Monoids.
 

algebra/CFields.v

@@ -40,7 +40,7 @@
 (** printing {1/} %\ensuremath{\frac1\cdot}% #1/# *)
 (** printing [/]?[//] %\ensuremath{/?\ddagger}% #/?‡# *)
 
-Require Export CRings.
+Require Export CoRN.algebra.CRings.
 Set Automatic Introduction.
 
 Transparent sym_eq.

algebra/CGroups.v

@@ -40,8 +40,8 @@
 (** printing {-} %\ensuremath-% #−# *)
 (** printing {--} %\ensuremath-% #−# *)
 
-Require Import CornTac.
-Require Export CMonoids.
+Require Import CoRN.tactics.CornTac.
+Require Export CoRN.algebra.CMonoids.
 Set Automatic Introduction.
 
 (* Begin_SpecReals *)

algebra/CMonoids.v

@@ -36,12 +36,12 @@
 
 (** printing [0] %\ensuremath{\mathbf0}% #0# *)
 
-Require Export Euclid.
-Require Export Cmod.
-Require Export CSemiGroups.
-Require Export csetoid_rewrite.
-Require Export Nsec.
-Require Import SetoidPermutation Setoid Morphisms.
+Require Export Coq.Arith.Euclid.
+Require Export CoRN.model.Zmod.Cmod.
+Require Export CoRN.algebra.CSemiGroups.
+Require Export CoRN.tactics.csetoid_rewrite.
+Require Export CoRN.model.structures.Nsec.
+Require Import CoRN.util.SetoidPermutation Coq.Setoids.Setoid Coq.Classes.Morphisms.
 
 (* Begin_SpecReals *)
 

algebra/COrdAbs.v

@@ -34,7 +34,7 @@
  * with this work; if not, write to the Free Software Foundation, Inc.,
  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  *)
-Require Export COrdFields2.
+Require Export CoRN.algebra.COrdFields2.
 
 (**
 ** Properties of [AbsSmall]

algebra/COrdCauchy.v

@@ -33,7 +33,7 @@
  * with this work; if not, write to the Free Software Foundation, Inc.,
  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  *)
-Require Export COrdAbs.
+Require Export CoRN.algebra.COrdAbs.
 Set Automatic Introduction.
 
 (* Begin_SpecReals *)

algebra/COrdFields.v

@@ -51,9 +51,9 @@
 (** printing TwentyFourNZ %\ensuremath{\mathbf{24}}% #24# *)
 (** printing FortyEightNZ %\ensuremath{\mathbf{48}}% #48# *)
 
-Require Export FieldReflection.
-Require Export CSetoids.
-Require Export Rational.
+Require Export CoRN.tactics.FieldReflection.
+Require Export CoRN.algebra.CSetoids.
+Require Export CoRN.tactics.Rational.
 
 (* ORDERED FIELDS *)
 

algebra/COrdFields2.v

@@ -33,7 +33,7 @@
  * with this work; if not, write to the Free Software Foundation, Inc.,
  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  *)
-Require Export COrdFields.
+Require Export CoRN.algebra.COrdFields.
 
 (** printing one_div_succ %\ensuremath{\frac1{\cdot+1}}% *)
 (** printing Half %\ensuremath{\frac12}% #½# *)

algebra/CPoly_ApZero.v

@@ -34,10 +34,10 @@
  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  *)
 
-Require Export CPoly_Degree.
-Require Export COrdFields2.
-Require Import Morphisms Permutation.
-Require ne_list.
+Require Export CoRN.algebra.CPoly_Degree.
+Require Export CoRN.algebra.COrdFields2.
+Require Import Coq.Classes.Morphisms Coq.Sorting.Permutation.
+Require MathClasses.implementations.ne_list.
 Import ne_list.notations.
 
 Set Automatic Introduction.

algebra/CPoly_Degree.v

@@ -34,9 +34,9 @@
  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  *)
 
-Require Export CPoly_NthCoeff.
-Require Export CFields.
-Require Export Rational.
+Require Export CoRN.algebra.CPoly_NthCoeff.
+Require Export CoRN.algebra.CFields.
+Require Export CoRN.tactics.Rational.
 Set Automatic Introduction.
 
 (**

algebra/CPoly_NthCoeff.v

@@ -34,9 +34,9 @@
  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  *)
 
-Require Export CPolynomials.
-Require Import Morphisms.
-Require Import CRings.
+Require Export CoRN.algebra.CPolynomials.
+Require Import Coq.Classes.Morphisms.
+Require Import CoRN.algebra.CRings.
 
 (**
 * Polynomials: Nth Coefficient

algebra/CPolynomials.v

@@ -40,8 +40,8 @@
 (** printing RX %\ensuremath{R[x]}% #R[x]# *)
 (** printing FX %\ensuremath{F[x]}% #F[x]# *)
 
-Require Import CRing_Homomorphisms.
-Require Import Rational.
+Require Import CoRN.algebra.CRing_Homomorphisms.
+Require Import CoRN.tactics.Rational.
 
 (**
 * Polynomials

algebra/CRing_Homomorphisms.v

@@ -46,7 +46,7 @@
 (** printing [1] %\ensuremath{\mathbf1}% #1# *)
 (** printing phi %\ensuremath{\phi}%  *)
 
-Require Export CRings.
+Require Export CoRN.algebra.CRings.
 Set Automatic Introduction.
 
 (**

algebra/CRing_as_Ring.v

@@ -1,5 +1,5 @@
 
-Require Export CRings Ring.
+Require Export CoRN.algebra.CRings Coq.setoid_ring.Ring.
 Definition CRing_Ring(R:CRing):(ring_theory (@cm_unit R) (@cr_one R) (@csg_op R) (@cr_mult R) (fun x y => x [-] y) (@cg_inv R) (@cs_eq R)).
 Proof.
  split;algebra.

algebra/CRings.v

@@ -53,9 +53,9 @@
 (** printing TwentyFour %\ensuremath{\mathbf{24}}% #24# *)
 (** printing FortyEight %\ensuremath{\mathbf{48}}% #48# *)
 
-Require Import CornTac.
-Require Export CSums.
-Require Import CAbMonoids Permutation SetoidPermutation Setoid Morphisms.
+Require Import CoRN.tactics.CornTac.
+Require Export CoRN.algebra.CSums.
+Require Import CoRN.algebra.CAbMonoids Coq.Sorting.Permutation CoRN.util.SetoidPermutation Coq.Setoids.Setoid Coq.Classes.Morphisms.
 
 Transparent sym_eq.
 Transparent f_equal.

algebra/CSemiGroups.v

@@ -37,7 +37,7 @@
 (** printing [+] %\ensuremath+% #+# *)
 (** printing {+} %\ensuremath+% #+# *)
 
-Require Export CSetoidInc.
+Require Export CoRN.algebra.CSetoidInc.
 
 (* Begin_SpecReals *)
 

algebra/CSetoidFun.v

@@ -34,7 +34,7 @@
  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  *)
 
-Require Export CSetoids.
+Require Export CoRN.algebra.CSetoids.
 
 (**
 ** The Setoid of Setoid functions

algebra/CSetoidInc.v

@@ -36,7 +36,7 @@
 
 (** printing included %\ensuremath{\subseteq}% #⊆# *)
 
-Require Export CSetoidFun.
+Require Export CoRN.algebra.CSetoidFun.
 
 Section inclusion.
 

algebra/CSetoids.v

@@ -50,10 +50,10 @@ Definition of a constructive setoid with apartness,
 i.e.%\% a set with an equivalence relation and an apartness relation compatible with it.
 *)
 
-Require Import CornTac.
-Require Export CLogic.
-Require Export Step.
-Require Export RSetoid.
+Require Import CoRN.tactics.CornTac.
+Require Export CoRN.logic.CLogic.
+Require Export CoRN.tactics.Step.
+Require Export CoRN.algebra.RSetoid.
 
 Delimit Scope corn_scope with corn.
 Open Scope corn_scope.

algebra/CSums.v

@@ -40,8 +40,8 @@
 (** printing Sum %\ensuremath{\sum}% #∑# *)
 (** printing Sumx %\ensuremath{\sum'}% #∑'&*)
 
-Require Export CAbGroups.
-Require Export Peano_dec.
+Require Export CoRN.algebra.CAbGroups.
+Require Export Coq.Arith.Peano_dec.
 
 (**
 * Sums