Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

V8.6 #19

Closed
wants to merge 5 commits into from
Closed

V8.6 #19

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
a659af8
fix a unused variable name warning
Zimmi48 Mar 14, 2017
1d426a0
Merge pull request #36 from Zimmi48/fix-for-coq-pr-474
spitters Apr 9, 2017
d2b2a04
math-classes : switch to the external Bignums library
letouzey Jun 6, 2017
1ad7358
Merge pull request #41 from letouzey/external-bignums
spitters Oct 26, 2017
3acda79
Merge pull request #43 from math-classes/master
spitters Oct 26, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
2 changes: 1 addition & 1 deletion implementations/NType_naturals.v
View file
Open in desktop
@@ -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.

Expand Down
2 changes: 1 addition & 1 deletion implementations/QType_rationals.v
View file
Open in desktop
@@ -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.
Expand Down
2 changes: 1 addition & 1 deletion implementations/ZType_integers.v
View file
Open in desktop
@@ -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.

Expand Down
2 changes: 1 addition & 1 deletion implementations/fast_integers.v
View file
Open in desktop
@@ -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
Expand Down
2 changes: 1 addition & 1 deletion implementations/fast_naturals.v
View file
Open in desktop
@@ -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.

Expand Down
2 changes: 1 addition & 1 deletion implementations/fast_rationals.v
View file
Open in desktop
@@ -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.
Expand Down
2 changes: 1 addition & 1 deletion theory/ua_subvariety.v
View file
Open in desktop
Expand Up @@ -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)...
Expand Down