Using the From X Require Y for v8.4

13 files changed, 24 insertions, 20 deletions

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.