Merge pull request #46 from Zimmi48/v8.6

V8.6

Author: spitters

.travis.yml

@@ -10,4 +10,6 @@ install:
   - sudo apt-get update && sudo apt-get install -y opam
   - opam init -y && eval $(opam config env) && opam config var root
   - travis_wait opam install -y coq
+  - opam repo add coq-released http://coq.inria.fr/opam/released
+  - opam install -y coq-bignums
 script: make

implementations/NType_naturals.v

@@ -1,7 +1,7 @@
 Require
   MathClasses.implementations.stdlib_binary_integers MathClasses.theory.integers MathClasses.orders.semirings.
 Require Import
-  Coq.Setoids.Setoid Coq.Numbers.Natural.SpecViaZ.NSig Coq.Numbers.Natural.SpecViaZ.NSigNAxioms Coq.NArith.NArith Coq.ZArith.ZArith Coq.Program.Program Coq.Classes.Morphisms
+  Coq.Setoids.Setoid Bignums.SpecViaZ.NSig Bignums.SpecViaZ.NSigNAxioms Coq.NArith.NArith Coq.ZArith.ZArith Coq.Program.Program Coq.Classes.Morphisms
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers
   MathClasses.interfaces.orders MathClasses.interfaces.additional_operations.
 

implementations/QType_rationals.v

@@ -1,7 +1,7 @@
 Require
   MathClasses.theory.fields MathClasses.implementations.stdlib_rationals MathClasses.theory.int_pow.
 Require Import
-  Coq.QArith.QArith Coq.Numbers.Rational.SpecViaQ.QSig
+  Coq.QArith.QArith Bignums.SpecViaQ.QSig
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders
   MathClasses.interfaces.integers MathClasses.interfaces.rationals MathClasses.interfaces.additional_operations
   MathClasses.theory.rings MathClasses.theory.rationals.

implementations/ZType_integers.v

@@ -1,7 +1,7 @@
 Require
   MathClasses.implementations.stdlib_binary_integers MathClasses.theory.integers MathClasses.orders.semirings.
 Require Import
-  Coq.Numbers.Integer.SpecViaZ.ZSig Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms Coq.NArith.NArith Coq.ZArith.ZArith
+  Bignums.SpecViaZ.ZSig Bignums.SpecViaZ.ZSigZAxioms Coq.NArith.NArith Coq.ZArith.ZArith
   MathClasses.implementations.nonneg_integers_naturals MathClasses.interfaces.orders
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.interfaces.additional_operations.
 

implementations/fast_integers.v

@@ -1,5 +1,5 @@
 Require Import
-  Coq.Numbers.Integer.BigZ.BigZ
+  Bignums.BigZ.BigZ
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers
   MathClasses.interfaces.additional_operations MathClasses.implementations.fast_naturals.
 Require Export

implementations/fast_naturals.v

@@ -1,5 +1,5 @@
 Require Import
-  Coq.Numbers.Natural.BigN.BigN MathClasses.interfaces.naturals.
+  Bignums.BigN.BigN MathClasses.interfaces.naturals.
 Require Export
   MathClasses.implementations.NType_naturals.
 

implementations/fast_rationals.v

@@ -1,7 +1,7 @@
 Require
   MathClasses.theory.shiftl MathClasses.theory.int_pow.
 Require Import
-  Coq.QArith.QArith Coq.Numbers.Rational.BigQ.BigQ
+  Coq.QArith.QArith Bignums.BigQ.BigQ
   MathClasses.interfaces.abstract_algebra
   MathClasses.interfaces.integers MathClasses.interfaces.rationals MathClasses.interfaces.additional_operations
   MathClasses.implementations.fast_naturals MathClasses.implementations.fast_integers MathClasses.implementations.field_of_fractions MathClasses.implementations.stdlib_rationals.

theory/ua_subvariety.v

@@ -72,7 +72,7 @@ Section contents.
    intros.
    generalize (@variety_laws et A _ _ _ s H1 (Pvars vars)). clear H1.
    destruct s as [x [? [t t0]]].
-   induction x as [A| [x1 [t1 t2]]]; simpl in *; intros.
+   induction x as [| [x1 [t1 t2]]]; simpl in *; intros.
     unfold equiv, sig_equiv.
     rewrite (heq_eval_const vars t).
     rewrite (heq_eval_const vars t0)...