Using the From X Require Y for v8.4

9 files changed, 24 insertions, 24 deletions

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.