Using the From X Require Y for v8.4

19 files changed, 64 insertions, 54 deletions

diff --git a/mathcomp/algebra/Makefile b/mathcomp/algebra/Makefile
index ead5950..e872352 100644
--- a/mathcomp/algebra/Makefile
+++ b/mathcomp/algebra/Makefile
@@ -4,20 +4,12 @@ ifeq "$(COQBIN)" ""
 COQBIN=$(dir $(shell which coqtop))/
 endif
 
-
-VERSION_Coq = $(shell $(COQBIN)/coqtop -v | head -1 | sed 's/.*version \([0-9]\.[0-9]\)[^ ]* .*/v\1/')
-
-ifeq "$(VERSION_Coq)" ""
-$(error no version number found for coq)
-endif
-
 OLD_MAKEFLAGS:=$(MAKEFLAGS)
 MAKEFLAGS+=-B
 
 .DEFAULT_GOAL := all
 
 %:
-	sed -i -e "s/^(\*$(VERSION_Coq) *\(.*\) *\*)/\1/" *.v
 	$(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq
 	$(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
 		-f Makefile.coq $*
diff --git a/mathcomp/algebra/cyclic.v b/mathcomp/algebra/cyclic.v
index caeb57f..4365406 100644
--- a/mathcomp/algebra/cyclic.v
+++ b/mathcomp/algebra/cyclic.v
@@ -1,9 +1,10 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-(*v8.5 From mathcomp.ssreflect *)
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
 Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
-(*v8.5 From mathcomp.discrete *)
+From mathcomp.discrete
 Require Import div fintype bigop prime finset.
-(*v8.5 From mathcomp.fingroup *)
+From mathcomp.fingroup
 Require Import fingroup morphism perm automorphism quotient gproduct.
 Require Import ssralg finalg zmodp poly.
 
diff --git a/mathcomp/algebra/finalg.v b/mathcomp/algebra/finalg.v
index d364fc9..13daa31 100644
--- a/mathcomp/algebra/finalg.v
+++ b/mathcomp/algebra/finalg.v
@@ -1,9 +1,10 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-(*v8.5 From mathcomp.ssreflect *)
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
 Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
-(*v8.5 From mathcomp.discrete *)
+From mathcomp.discrete
 Require Import choice fintype finset.
-(*v8.5 From mathcomp.fingroup *)
+From mathcomp.fingroup
 Require Import fingroup morphism perm action.
 Require Import ssralg.
 
diff --git a/mathcomp/algebra/fraction.v b/mathcomp/algebra/fraction.v
index 446248f..9ce2718 100644
--- a/mathcomp/algebra/fraction.v
+++ b/mathcomp/algebra/fraction.v
@@ -1,7 +1,8 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-(*v8.5 From mathcomp.ssreflect *)
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
 Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
-(*v8.5 From mathcomp.discrete *)
+From mathcomp.discrete
 Require Import div choice tuple bigop generic_quotient.
 Require Import ssralg poly polydiv.
 
diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v
index bfd4b13..cdfde3c 100644
--- a/mathcomp/algebra/intdiv.v
+++ b/mathcomp/algebra/intdiv.v
@@ -1,9 +1,10 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-(*v8.5 From mathcomp.ssreflect *)
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
 Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
-(*v8.5 From mathcomp.discrete *)
+From mathcomp.discrete
 Require Import path div choice fintype tuple finfun bigop prime.
-(*v8.5 From mathcomp.fingroup *)
+From mathcomp.fingroup
 Require Import perm.
 Require Import ssralg poly ssrnum ssrint rat.
 Require Import polydiv finalg zmodp matrix mxalgebra vector.
diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v
index 7bde270..bed19fa 100644
--- a/mathcomp/algebra/interval.v
+++ b/mathcomp/algebra/interval.v
@@ -1,9 +1,10 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-(*v8.5 From mathcomp.ssreflect *)
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
 Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
-(*v8.5 From mathcomp.discrete *)
+From mathcomp.discrete
 Require Import div choice fintype bigop finset.
-(*v8.5 From mathcomp.fingroup *)
+From mathcomp.fingroup
 Require Import fingroup.
 Require Import ssralg zmodp ssrint ssrnum.
 
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index e67008d..9339e67 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -1,9 +1,10 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-(*v8.5 From mathcomp.ssreflect *)
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
 Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
-(*v8.5 From mathcomp.discrete *)
+From mathcomp.discrete
 Require Import  div choice fintype finfun bigop prime binomial finset.
-(*v8.5 From mathcomp.fingroup *)
+From mathcomp.fingroup
 Require Import fingroup perm.
 Require Import ssralg finalg zmodp.
 
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index 833a229..cb1717c 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -1,9 +1,10 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-(*v8.5 From mathcomp.ssreflect *)
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
 Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
-(*v8.5 From mathcomp.discrete *)
+From mathcomp.discrete
 Require Import div choice fintype finfun bigop prime binomial finset.
-(*v8.5 From mathcomp.fingroup *)
+From mathcomp.fingroup
 Require Import fingroup perm.
 Require Import ssralg finalg zmodp matrix.
 
diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v
index 8a0b519..bc5a998 100644
--- a/mathcomp/algebra/mxpoly.v
+++ b/mathcomp/algebra/mxpoly.v
@@ -1,9 +1,10 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-(*v8.5 From mathcomp.ssreflect *)
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
 Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
-(*v8.5 From mathcomp.discrete *)
+From mathcomp.discrete
 Require Import div fintype tuple finfun bigop.
-(*v8.5 From mathcomp.fingroup *)
+From mathcomp.fingroup
 Require Import fingroup perm.
 Require Import ssralg zmodp matrix mxalgebra poly polydiv.
 
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index e473f2d..2757b30 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -1,7 +1,8 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-(*v8.5 From mathcomp.ssreflect *)
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
 Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
-(*v8.5 From mathcomp.discrete *)
+From mathcomp.discrete
 Require Import div choice fintype bigop binomial.
 Require Import ssralg.
 
diff --git a/mathcomp/algebra/polyXY.v b/mathcomp/algebra/polyXY.v
index 5abc40d..d79b2bf 100644
--- a/mathcomp/algebra/polyXY.v
+++ b/mathcomp/algebra/polyXY.v
@@ -1,9 +1,10 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-(*v8.5 From mathcomp.ssreflect *)
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
 Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
-(*v8.5 From mathcomp.discrete *)
+From mathcomp.discrete
 Require Import choice div fintype tuple finfun bigop binomial.
-(*v8.5 From mathcomp.fingroup *)
+From mathcomp.fingroup
 Require Import fingroup perm.
 Require Import ssralg zmodp matrix mxalgebra poly polydiv mxpoly.
 
diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v
index fa3a132..5910586 100644
--- a/mathcomp/algebra/polydiv.v
+++ b/mathcomp/algebra/polydiv.v
@@ -1,7 +1,8 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-(*v8.5 From mathcomp.ssreflect *)
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
 Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
-(*v8.5 From mathcomp.discrete *)
+From mathcomp.discrete
 Require Import bigop choice fintype.
 Require Import ssralg poly.
 
diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v
index 342eead..398d8de 100644
--- a/mathcomp/algebra/rat.v
+++ b/mathcomp/algebra/rat.v
@@ -1,7 +1,8 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-(*v8.5 From mathcomp.ssreflect *)
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
 Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
-(*v8.5 From mathcomp.discrete *)
+From mathcomp.discrete
 Require Import div choice fintype bigop.
 Require Import ssralg ssrnum ssrint.
 
diff --git a/mathcomp/algebra/ring_quotient.v b/mathcomp/algebra/ring_quotient.v
index 6f2a2f5..ea41744 100644
--- a/mathcomp/algebra/ring_quotient.v
+++ b/mathcomp/algebra/ring_quotient.v
@@ -1,7 +1,8 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-(*v8.5 From mathcomp.ssreflect *)
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
 Require Import ssreflect ssrfun ssrbool ssrnat eqtype seq.
-(*v8.5 From mathcomp.discrete *)
+From mathcomp.discrete
 Require Import choice generic_quotient.
 Require Import ssralg.
 
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index 3627447..820a4b9 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -1,7 +1,8 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-(*v8.5 From mathcomp.ssreflect *)
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
 Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
-(*v8.5 From mathcomp.discrete *)
+From mathcomp.discrete
 Require Import div choice fintype finfun bigop prime binomial.
 
 (******************************************************************************)
diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v
index 3281c44..48c78dd 100644
--- a/mathcomp/algebra/ssrint.v
+++ b/mathcomp/algebra/ssrint.v
@@ -1,7 +1,8 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-(*v8.5 From mathcomp.ssreflect *)
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
 Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
-(*v8.5 From mathcomp.discrete *)
+From mathcomp.discrete
 Require Import choice fintype finfun bigop.
 Require Import ssralg ssrnum poly.
 
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index 19d4c31..aecb910 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -1,9 +1,10 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-(*v8.5 From mathcomp.ssreflect *)
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
 Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
-(*v8.5 From mathcomp.discrete *)
+From mathcomp.discrete
 Require Import div choice fintype bigop finset.
-(*v8.5 From mathcomp.fingroup *)
+From mathcomp.fingroup
 Require Import fingroup.
 Require Import ssralg zmodp poly.
 
diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v
index 0d4ace0..01f2f53 100644
--- a/mathcomp/algebra/vector.v
+++ b/mathcomp/algebra/vector.v
@@ -1,7 +1,8 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-(*v8.5 From mathcomp.ssreflect *)
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
 Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
-(*v8.5 From mathcomp.discrete *)
+From mathcomp.discrete
 Require Import choice fintype bigop finfun tuple.
 Require Import ssralg matrix mxalgebra zmodp.
 
diff --git a/mathcomp/algebra/zmodp.v b/mathcomp/algebra/zmodp.v
index 614bf10..9dd3ff5 100644
--- a/mathcomp/algebra/zmodp.v
+++ b/mathcomp/algebra/zmodp.v
@@ -1,9 +1,10 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-(*v8.5 From mathcomp.ssreflect *)
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
 Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
-(*v8.5 From mathcomp.discrete *)
+From mathcomp.discrete
 Require Import  div fintype bigop finset prime.
-(*v8.5 From mathcomp.fingroup *)
+From mathcomp.fingroup
 Require Import fingroup.
 Require Import ssralg finalg.