merge basic/ into ssreflect/

25 files changed, 36 insertions, 108 deletions

diff --git a/mathcomp/Make b/mathcomp/Make
index d8fb252..66160b4 100644
--- a/mathcomp/Make
+++ b/mathcomp/Make
@@ -17,19 +17,6 @@ algebra/ssrnum.v
 algebra/vector.v
 algebra/zmodp.v
 all/all.v
-basic/all_basic.v
-basic/bigop.v
-basic/binomial.v
-basic/choice.v
-basic/div.v
-basic/finfun.v
-basic/fingraph.v
-basic/finset.v
-basic/fintype.v
-basic/generic_quotient.v
-basic/path.v
-basic/prime.v
-basic/tuple.v
 character/all_character.v
 character/character.v
 character/classfun.v
@@ -125,13 +112,25 @@ solvable/pgroup.v
 solvable/primitive_action.v
 solvable/sylow.v
 ssreflect/all_ssreflect.v
+ssreflect/bigop.v
+ssreflect/binomial.v
+ssreflect/choice.v
+ssreflect/div.v
 ssreflect/eqtype.v
+ssreflect/finfun.v
+ssreflect/fingraph.v
+ssreflect/finset.v
+ssreflect/fintype.v
+ssreflect/generic_quotient.v
+ssreflect/path.v
+ssreflect/prime.v
 ssreflect/seq.v
 ssreflect/ssrbool.v
 ssreflect/ssreflect.v
 ssreflect/ssrfun.v
 ssreflect/ssrmatching.v
 ssreflect/ssrnat.v
+ssreflect/tuple.v
 ssrtest/absevarprop.v
 ssrtest/binders_of.v
 ssrtest/binders.v
diff --git a/mathcomp/all/all.v b/mathcomp/all/all.v
index b860e17..391a342 100644
--- a/mathcomp/all/all.v
+++ b/mathcomp/all/all.v
@@ -1,5 +1,4 @@
 Require Export mathcomp.ssreflect.all_ssreflect.
-Require Export mathcomp.basic.all_basic.
 Require Export mathcomp.algebra.all_algebra.
 Require Export mathcomp.field.all_field.
 Require Export mathcomp.character.all_character.
diff --git a/mathcomp/basic/AUTHORS b/mathcomp/basic/AUTHORS
deleted file mode 120000
index b55a98d..0000000
--- a/mathcomp/basic/AUTHORS
+++ /dev/null
@@ -1 +0,0 @@
-../../etc/AUTHORS
\ No newline at end of file
diff --git a/mathcomp/basic/CeCILL-B b/mathcomp/basic/CeCILL-B
deleted file mode 120000
index 83e22fd..0000000
--- a/mathcomp/basic/CeCILL-B
+++ /dev/null
@@ -1 +0,0 @@
-../../etc/CeCILL-B
\ No newline at end of file
diff --git a/mathcomp/basic/INSTALL b/mathcomp/basic/INSTALL
deleted file mode 120000
index 6aa7ec5..0000000
--- a/mathcomp/basic/INSTALL
+++ /dev/null
@@ -1 +0,0 @@
-../../etc/INSTALL
\ No newline at end of file
diff --git a/mathcomp/basic/Make b/mathcomp/basic/Make
deleted file mode 100644
index 8acef84..0000000
--- a/mathcomp/basic/Make
+++ /dev/null
@@ -1,15 +0,0 @@
-all_basic.v
-bigop.v
-binomial.v
-choice.v
-div.v
-finfun.v
-fingraph.v
-finset.v
-fintype.v
-generic_quotient.v
-path.v
-prime.v
-tuple.v
-
--R . mathcomp.basic
\ No newline at end of file
diff --git a/mathcomp/basic/Makefile b/mathcomp/basic/Makefile
deleted file mode 100644
index 8f03823..0000000
--- a/mathcomp/basic/Makefile
+++ /dev/null
@@ -1,42 +0,0 @@
-H=@
-
-ifeq "$(COQBIN)" ""
-COQBIN=$(dir $(shell which coqtop))/
-endif
-
-BRANCH_coq = $(shell $(COQBIN)/coqtop -v | head -1 | sed 's/.*version \([0-9]\.[0-9]\)[^ ]* .*/v\1/')
-
-HASH_coq = $(shell echo Quit. | $(COQBIN)/coqtop 2>&1 | head -1 | sed 's/^.*(\([a-f0-9]*\)).*/\1/' )
-
-HASH_coq_v85beta1 = eaa3d0b15adf4eb11ffb00ab087746a5b15c4d5d
-
-
-ifeq "$(HASH_coq)" "$(HASH_coq_v85beta1)"
-V=v8.5beta1
-else
-V=$(BRANCH_coq)
-endif
-
-ifeq "$V" "v8.4"
-COQDEP=../../etc/utils/ssrcoqdep
-else
-COQDEP=$(COQBIN)/coqdep
-endif
-
-OLD_MAKEFLAGS:=$(MAKEFLAGS)
-MAKEFLAGS+=-B
-
-.DEFAULT_GOAL := all
-
-%:
-	$(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq
-	$(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
-		-f Makefile.coq $* \
-		COQDEP='$(COQDEP) -c'
-
-.PHONY: clean
-clean:
-	$(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
-		-f Makefile.coq clean
-	$(H)rm -f Makefile.coq
-
diff --git a/mathcomp/basic/README b/mathcomp/basic/README
deleted file mode 120000
index e4e30e8..0000000
--- a/mathcomp/basic/README
+++ /dev/null
@@ -1 +0,0 @@
-../../etc/README
\ No newline at end of file
diff --git a/mathcomp/basic/all_basic.v b/mathcomp/basic/all_basic.v
deleted file mode 100644
index dfa8536..0000000
--- a/mathcomp/basic/all_basic.v
+++ /dev/null
@@ -1,12 +0,0 @@
-Require Export choice.
-Require Export path.
-Require Export div.
-Require Export fintype.
-Require Export fingraph.
-Require Export tuple.
-Require Export finfun.
-Require Export bigop.
-Require Export prime.
-Require Export finset.
-Require Export binomial.
-Require Export generic_quotient.
diff --git a/mathcomp/basic/descr b/mathcomp/basic/descr
deleted file mode 100644
index 8bbc61e..0000000
--- a/mathcomp/basic/descr
+++ /dev/null
@@ -1,5 +0,0 @@
-Mathematical Components Library, basic restults
-
-This library contains definitions and theorems about finite types,
-finite sets, finite functions, finite graphs, basic arithmetics and
-prime numbers, big operators...
\ No newline at end of file
diff --git a/mathcomp/basic/opam b/mathcomp/basic/opam
deleted file mode 100644
index b7fcf08..0000000
--- a/mathcomp/basic/opam
+++ /dev/null
@@ -1,16 +0,0 @@
-opam-version: "1.2"
-name: "coq:mathcomp:basic"
-version: "dev"
-maintainer: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
-
-homepage: "http://ssr.msr-inria.inria.fr/"
-bug-reports: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
-license: "CeCILL-B"
-
-build: [ make "-j" "%{jobs}%" ]
-install: [ make "install" ]
-remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp/basic'" ]
-depends: [ "coq:mathcomp:ssreflect" { = "dev" } ]
-
-tags: [ "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" ]
-authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ]
diff --git a/mathcomp/ssreflect/Make b/mathcomp/ssreflect/Make
index 39f593b..4dd672c 100644
--- a/mathcomp/ssreflect/Make
+++ b/mathcomp/ssreflect/Make
@@ -6,6 +6,18 @@ ssreflect.v
 ssrfun.v
 ssrmatching.v
 ssrnat.v
+bigop.v
+binomial.v
+choice.v
+div.v
+finfun.v
+fingraph.v
+finset.v
+fintype.v
+generic_quotient.v
+path.v
+prime.v
+tuple.v
 
 ssreflect.mllib
 ssrmatching.mli
diff --git a/mathcomp/ssreflect/all_ssreflect.v b/mathcomp/ssreflect/all_ssreflect.v
index ce3e470..aae57ca 100644
--- a/mathcomp/ssreflect/all_ssreflect.v
+++ b/mathcomp/ssreflect/all_ssreflect.v
@@ -4,3 +4,15 @@ Require Export ssrfun.
 Require Export eqtype.
 Require Export ssrnat.
 Require Export seq.
+Require Export choice.
+Require Export path.
+Require Export div.
+Require Export fintype.
+Require Export fingraph.
+Require Export tuple.
+Require Export finfun.
+Require Export bigop.
+Require Export prime.
+Require Export finset.
+Require Export binomial.
+Require Export generic_quotient.
diff --git a/mathcomp/basic/bigop.v b/mathcomp/ssreflect/bigop.v
index 5fed5bb..5fed5bb 100644
--- a/mathcomp/basic/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
diff --git a/mathcomp/basic/binomial.v b/mathcomp/ssreflect/binomial.v
index a136bfd..a136bfd 100644
--- a/mathcomp/basic/binomial.v
+++ b/mathcomp/ssreflect/binomial.v
diff --git a/mathcomp/basic/choice.v b/mathcomp/ssreflect/choice.v
index 4146634..4146634 100644
--- a/mathcomp/basic/choice.v
+++ b/mathcomp/ssreflect/choice.v
diff --git a/mathcomp/basic/div.v b/mathcomp/ssreflect/div.v
index e858d54..e858d54 100644
--- a/mathcomp/basic/div.v
+++ b/mathcomp/ssreflect/div.v
diff --git a/mathcomp/basic/finfun.v b/mathcomp/ssreflect/finfun.v
index ca148e2..ca148e2 100644
--- a/mathcomp/basic/finfun.v
+++ b/mathcomp/ssreflect/finfun.v
diff --git a/mathcomp/basic/fingraph.v b/mathcomp/ssreflect/fingraph.v
index 54dde32..54dde32 100644
--- a/mathcomp/basic/fingraph.v
+++ b/mathcomp/ssreflect/fingraph.v
diff --git a/mathcomp/basic/finset.v b/mathcomp/ssreflect/finset.v
index 6fa29ff..6fa29ff 100644
--- a/mathcomp/basic/finset.v
+++ b/mathcomp/ssreflect/finset.v
diff --git a/mathcomp/basic/fintype.v b/mathcomp/ssreflect/fintype.v
index 29d1f3e..29d1f3e 100644
--- a/mathcomp/basic/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
diff --git a/mathcomp/basic/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v
index d78e0d8..d78e0d8 100644
--- a/mathcomp/basic/generic_quotient.v
+++ b/mathcomp/ssreflect/generic_quotient.v
diff --git a/mathcomp/basic/path.v b/mathcomp/ssreflect/path.v
index ec81f81..ec81f81 100644
--- a/mathcomp/basic/path.v
+++ b/mathcomp/ssreflect/path.v
diff --git a/mathcomp/basic/prime.v b/mathcomp/ssreflect/prime.v
index b346a93..b346a93 100644
--- a/mathcomp/basic/prime.v
+++ b/mathcomp/ssreflect/prime.v
diff --git a/mathcomp/basic/tuple.v b/mathcomp/ssreflect/tuple.v
index a6a154f..a6a154f 100644
--- a/mathcomp/basic/tuple.v
+++ b/mathcomp/ssreflect/tuple.v