Using the From X Require Y for v8.4

49 files changed, 112 insertions, 161 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.
 
diff --git a/mathcomp/all/Makefile b/mathcomp/all/Makefile
index ead5950..e872352 100644
--- a/mathcomp/all/Makefile
+++ b/mathcomp/all/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/attic/Makefile b/mathcomp/attic/Makefile
index ead5950..e872352 100644
--- a/mathcomp/attic/Makefile
+++ b/mathcomp/attic/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/character/Makefile b/mathcomp/character/Makefile
index ead5950..e872352 100644
--- a/mathcomp/character/Makefile
+++ b/mathcomp/character/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/discrete/Makefile b/mathcomp/discrete/Makefile
index ead5950..e872352 100644
--- a/mathcomp/discrete/Makefile
+++ b/mathcomp/discrete/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/discrete/bigop.v b/mathcomp/discrete/bigop.v
index f8bee66..8a25624 100644
--- a/mathcomp/discrete/bigop.v
+++ b/mathcomp/discrete/bigop.v
@@ -1,5 +1,6 @@
 (* (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.
 Require Import  path div fintype tuple finfun.
 
diff --git a/mathcomp/discrete/binomial.v b/mathcomp/discrete/binomial.v
index 0c380da..51b9635 100644
--- a/mathcomp/discrete/binomial.v
+++ b/mathcomp/discrete/binomial.v
@@ -1,5 +1,6 @@
 (* (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.
 Require Import  path div fintype tuple finfun bigop prime finset.
 
diff --git a/mathcomp/discrete/choice.v b/mathcomp/discrete/choice.v
index 6793837..5909752 100644
--- a/mathcomp/discrete/choice.v
+++ b/mathcomp/discrete/choice.v
@@ -1,5 +1,6 @@
 (* (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.
 
 (******************************************************************************)
diff --git a/mathcomp/discrete/div.v b/mathcomp/discrete/div.v
index 5bf57dd..8ffa036 100644
--- a/mathcomp/discrete/div.v
+++ b/mathcomp/discrete/div.v
@@ -1,5 +1,6 @@
 (* (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.
 
 (******************************************************************************)
diff --git a/mathcomp/discrete/finfun.v b/mathcomp/discrete/finfun.v
index 98bc5ca..849bbe2 100644
--- a/mathcomp/discrete/finfun.v
+++ b/mathcomp/discrete/finfun.v
@@ -1,5 +1,6 @@
 (* (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.
 Require Import choice fintype tuple.
 
diff --git a/mathcomp/discrete/fingraph.v b/mathcomp/discrete/fingraph.v
index a111adc..34167d0 100644
--- a/mathcomp/discrete/fingraph.v
+++ b/mathcomp/discrete/fingraph.v
@@ -1,5 +1,6 @@
 (* (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.
 Require Import path fintype.
 
diff --git a/mathcomp/discrete/finset.v b/mathcomp/discrete/finset.v
index a4bdc89..78c1753 100644
--- a/mathcomp/discrete/finset.v
+++ b/mathcomp/discrete/finset.v
@@ -1,5 +1,6 @@
 (* (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.
 Require Import bigop choice fintype div finfun.
 
diff --git a/mathcomp/discrete/fintype.v b/mathcomp/discrete/fintype.v
index 2a65c4f..347c823 100644
--- a/mathcomp/discrete/fintype.v
+++ b/mathcomp/discrete/fintype.v
@@ -1,5 +1,6 @@
 (* (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.
 Require Import choice.
 
diff --git a/mathcomp/discrete/generic_quotient.v b/mathcomp/discrete/generic_quotient.v
index d16f43d..38696d8 100644
--- a/mathcomp/discrete/generic_quotient.v
+++ b/mathcomp/discrete/generic_quotient.v
@@ -1,6 +1,7 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
 (* -*- coding : utf-8 -*- *)
-(*v8.5 From mathcomp.ssreflect   *)
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect  
 Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
 Require Import choice fintype.
 
diff --git a/mathcomp/discrete/path.v b/mathcomp/discrete/path.v
index d5e3864..cea608f 100644
--- a/mathcomp/discrete/path.v
+++ b/mathcomp/discrete/path.v
@@ -1,5 +1,6 @@
 (* (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.
 
 (******************************************************************************)
diff --git a/mathcomp/discrete/prime.v b/mathcomp/discrete/prime.v
index fde2309..4c3bdf8 100644
--- a/mathcomp/discrete/prime.v
+++ b/mathcomp/discrete/prime.v
@@ -1,5 +1,6 @@
 (* (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.
 Require Import path fintype div bigop.
 
diff --git a/mathcomp/discrete/tuple.v b/mathcomp/discrete/tuple.v
index 6847df4..450106a 100644
--- a/mathcomp/discrete/tuple.v
+++ b/mathcomp/discrete/tuple.v
@@ -1,5 +1,6 @@
 (* (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.
 Require Import choice fintype.
 
diff --git a/mathcomp/field/Makefile b/mathcomp/field/Makefile
index ead5950..e872352 100644
--- a/mathcomp/field/Makefile
+++ b/mathcomp/field/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/fingroup/Makefile b/mathcomp/fingroup/Makefile
index ead5950..e872352 100644
--- a/mathcomp/fingroup/Makefile
+++ b/mathcomp/fingroup/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/fingroup/action.v b/mathcomp/fingroup/action.v
index 09c7d75..3e92be4 100644
--- a/mathcomp/fingroup/action.v
+++ b/mathcomp/fingroup/action.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 fintype bigop finset.
 Require Import fingroup morphism perm automorphism quotient.
 
diff --git a/mathcomp/fingroup/automorphism.v b/mathcomp/fingroup/automorphism.v
index d61928b..8c9b0b9 100644
--- a/mathcomp/fingroup/automorphism.v
+++ b/mathcomp/fingroup/automorphism.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.
-(*v8.5 From mathcomp.discrete *)
+From mathcomp.discrete
 Require Import fintype finset.
 Require Import fingroup perm morphism.
 
diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v
index 40b5137..9044cd0 100644
--- a/mathcomp/fingroup/fingroup.v
+++ b/mathcomp/fingroup/fingroup.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  choice fintype div path bigop prime finset.
 
 (******************************************************************************)
diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v
index 3c69df5..2706df6 100644
--- a/mathcomp/fingroup/gproduct.v
+++ b/mathcomp/fingroup/gproduct.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 finset.
 Require Import fingroup morphism quotient action.
 
diff --git a/mathcomp/fingroup/morphism.v b/mathcomp/fingroup/morphism.v
index e7ce6b1..9649644 100644
--- a/mathcomp/fingroup/morphism.v
+++ b/mathcomp/fingroup/morphism.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 choice fintype finfun bigop finset.
 Require Import fingroup.
 
diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v
index ec6df27..3719835 100644
--- a/mathcomp/fingroup/perm.v
+++ b/mathcomp/fingroup/perm.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 path choice fintype tuple finfun bigop finset binomial.
 Require Import fingroup.
 
diff --git a/mathcomp/fingroup/presentation.v b/mathcomp/fingroup/presentation.v
index a7a0efe..8f6ddb3 100644
--- a/mathcomp/fingroup/presentation.v
+++ b/mathcomp/fingroup/presentation.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 fintype finset.
 Require Import fingroup morphism.
 
diff --git a/mathcomp/fingroup/quotient.v b/mathcomp/fingroup/quotient.v
index 204d75e..1983e59 100644
--- a/mathcomp/fingroup/quotient.v
+++ b/mathcomp/fingroup/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 eqtype ssrnat seq.
-(*v8.5 From mathcomp.discrete *)
+From mathcomp.discrete
 Require Import div choice fintype prime finset.
 Require Import fingroup morphism automorphism.
 
diff --git a/mathcomp/odd_order/Makefile b/mathcomp/odd_order/Makefile
index ead5950..e872352 100644
--- a/mathcomp/odd_order/Makefile
+++ b/mathcomp/odd_order/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/real_closed/Makefile b/mathcomp/real_closed/Makefile
index ead5950..e872352 100644
--- a/mathcomp/real_closed/Makefile
+++ b/mathcomp/real_closed/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/solvable/Makefile b/mathcomp/solvable/Makefile
index ead5950..e872352 100644
--- a/mathcomp/solvable/Makefile
+++ b/mathcomp/solvable/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/ssrtest/Makefile b/mathcomp/ssrtest/Makefile
index 3614d33..4bcf4fb 100644
--- a/mathcomp/ssrtest/Makefile
+++ b/mathcomp/ssrtest/Makefile
@@ -7,12 +7,6 @@ MAKEFLAGS := -r
 COQMAKEFILE := Makefile.coq
 COQMAKE := +$(MAKE) -f $(COQMAKEFILE)
 
-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
-
 all: $(COQMAKEFILE)
 	$(COQMAKE) all
 
@@ -29,5 +23,4 @@ tags:
 install:
 
 %: Makefile.coq
-	sed -i -e "s/^(\*$(VERSION_Coq) *\(.*\) *\*)/\1/" *.v
 	$(COQMAKE) $@