Merge pull request #24 from bmsherman/imports

Make import statements absolute and other small changes

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

algebra/Cauchy_COF.v

@@ -34,8 +34,8 @@
  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  *)
 
-Require Export COrdCauchy.
-Require Export RingReflection.
+Require Export CoRN.algebra.COrdCauchy.
+Require Export CoRN.tactics.RingReflection.
 
 (**
 * The Field of Cauchy Sequences

algebra/CornScope.v

@@ -1,4 +1,4 @@
-Require Export CSetoids.
+Require Export CoRN.algebra.CSetoids.
 Delimit Scope corn_scope with corn.
 (* Open Scope corn_scope.*)
 
@@ -8,20 +8,20 @@ Arguments Scope cs_eq [ _ corn_scope corn_scope].
 (* Infix "#" := cs_ap (at level 70, no associativity) : corn_scope. *)
 Infix "==" := cs_eq (at level 70, no associativity) : corn_scope.
 
-Require Import CSemiGroups.
+Require Import CoRN.algebra.CSemiGroups.
 Arguments Scope csg_op [ _ corn_scope corn_scope ].
 Infix "+" := csg_op (at level 50, left associativity) : corn_scope.
 
 
-Require Import CMonoids.
+Require Import CoRN.algebra.CMonoids.
 Notation "0" := (cm_unit _) : corn_scope.
 Notation "(+)" := csg_op (only parsing) : corn_scope.
 
-Require Import CGroups.
+Require Import CoRN.algebra.CGroups.
 Notation "- x" := (cg_inv x) (at level 35, right associativity) : corn_scope.
 Infix "-" := cg_minus (at level 50, left associativity) : corn_scope.
 
-Require Import CRings.
+Require Import CoRN.algebra.CRings.
 Arguments Scope cr_mult [ _ corn_scope corn_scope ].
 Infix "*" := cr_mult (at level 40, left associativity) : corn_scope.
 Notation "x ^ n" := (nexp_op _ n x) : corn_scope.

algebra/Expon.v

@@ -36,8 +36,8 @@
 
 (** printing [^^] %\ensuremath{\hat{\ }}% #^# *)
 
-Require Export Arith.
-Require Export COrdCauchy.
+Require Export Coq.Arith.Arith.
+Require Export CoRN.algebra.COrdCauchy.
 
 Load "Transparent_algebra".
 

algebra/OperationClasses.v

@@ -19,7 +19,7 @@ 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 Import Setoid Morphisms.
+Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms.
 Notation " x === y " := (Equivalence.equiv x y) (at level 70, no associativity).
 
 Set Implicit Arguments.

algebra/RSetoid.v

@@ -21,9 +21,9 @@ CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
 
 Set Implicit Arguments.
 
-Require Export Setoid.
-Require Import CornBasics.
-Require Import abstract_algebra.
+Require Export Coq.Setoids.Setoid.
+Require Import CoRN.logic.CornBasics.
+Require Import MathClasses.interfaces.abstract_algebra.
 
 (* Require Import CornTac.*)
 

classes/Qclasses.v

@@ -1,9 +1,9 @@
 Require Import 
-  QMinMax
-  abstract_algebra
-  minmax.
+  CoRN.model.totalorder.QMinMax
+  MathClasses.interfaces.abstract_algebra
+  MathClasses.orders.minmax.
 Require Export 
-  stdlib_rationals.
+  MathClasses.implementations.stdlib_rationals.
 
 Lemma Qmin_coincides x y : Qmin x y = x ⊓ y.
 Proof.

classes/Qposclasses.v

@@ -1,7 +1,7 @@
 (* todo: remove *)
 
-Require Export Qpossec.
-Require Import abstract_algebra additional_operations stdlib_rationals.
+Require Export CoRN.model.structures.Qpossec.
+Require Import MathClasses.interfaces.abstract_algebra MathClasses.interfaces.additional_operations MathClasses.implementations.stdlib_rationals.
 
 Instance: Equiv Qpos := QposEq.
 Instance: One Qpos := Qpos_one.

complex/AbsCC.v

@@ -34,7 +34,7 @@
  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  *)
 
-Require Export CComplex.
+Require Export CoRN.complex.CComplex.
 
 (**
 * Absolute value on [CC]

complex/CComplex.v

@@ -42,7 +42,7 @@
 (** printing AbsCC %\ensuremath{|\cdot|_{\mathbb C}}% *)
 (** printing CCX %\ensuremath{\mathbb C[X]}% #<b>C</b>[X]# *)
 
-Require Export NRootIR.
+Require Export CoRN.reals.NRootIR.
 
 (**
 * Complex Numbers

complex/Complex_Exponential.v

@@ -36,9 +36,9 @@
 
 (** printing ExpCC %\ensuremath{\exp_{\mathbb C}}% *)
 
-Require Export AbsCC.
-Require Export Exponential.
-Require Export Pi.
+Require Export CoRN.complex.AbsCC.
+Require Export CoRN.transc.Exponential.
+Require Export CoRN.transc.Pi.
 
 (**
 ** The Complex Exponential *)

complex/NRootCC.v

@@ -39,9 +39,9 @@
 (** printing nroot_I %\ensuremath{\sqrt[n]{\imath}}% *)
 (** printing nroot_minus_I %\ensuremath{\sqrt[n]{-\imath}}% *)
 
-Require Export CComplex.
-Require Export Wf_nat.
-Require Export ArithRing.
+Require Export CoRN.complex.CComplex.
+Require Export Coq.Arith.Wf_nat.
+Require Export Coq.setoid_ring.ArithRing.
 
 (**
 * Roots of Complex Numbers