13 files changed, 19 insertions, 12 deletions
diff --git a/mathcomp/discrete/Makefile b/mathcomp/discrete/Makefile
index d693257..ead5950 100644
--- a/mathcomp/discrete/Makefile
+++ b/mathcomp/discrete/Makefile
@@ -5,12 +5,19 @@ 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 b6d77ec..f8bee66 100644
--- a/mathcomp/discrete/bigop.v
+++ b/mathcomp/discrete/bigop.v
@@ -1,5 +1,5 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-(*v8.5 From mathcomp.ssreflect  *)
+(*v8.5 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 5656b30..0c380da 100644
--- a/mathcomp/discrete/binomial.v
+++ b/mathcomp/discrete/binomial.v
@@ -1,5 +1,5 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-(*v8.5 From mathcomp.ssreflect  *)
+(*v8.5 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 cfd0b58..6793837 100644
--- a/mathcomp/discrete/choice.v
+++ b/mathcomp/discrete/choice.v
@@ -1,5 +1,5 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-(*v8.5 From mathcomp.ssreflect   *)
+(*v8.5 From mathcomp.ssreflect    *)
 Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
 
 (******************************************************************************)
diff --git a/mathcomp/discrete/div.v b/mathcomp/discrete/div.v
index 0d94936..5bf57dd 100644
--- a/mathcomp/discrete/div.v
+++ b/mathcomp/discrete/div.v
@@ -1,5 +1,5 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-(*v8.5 From mathcomp.ssreflect  *)
+(*v8.5 From mathcomp.ssreflect   *)
 Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
 
 (******************************************************************************)
diff --git a/mathcomp/discrete/finfun.v b/mathcomp/discrete/finfun.v
index e6c6afc..98bc5ca 100644
--- a/mathcomp/discrete/finfun.v
+++ b/mathcomp/discrete/finfun.v
@@ -1,5 +1,5 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-(*v8.5 From mathcomp.ssreflect  *)
+(*v8.5 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 d445510..a111adc 100644
--- a/mathcomp/discrete/fingraph.v
+++ b/mathcomp/discrete/fingraph.v
@@ -1,5 +1,5 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-(*v8.5 From mathcomp.ssreflect  *)
+(*v8.5 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 5067701..a4bdc89 100644
--- a/mathcomp/discrete/finset.v
+++ b/mathcomp/discrete/finset.v
@@ -1,5 +1,5 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-(*v8.5 From mathcomp.ssreflect  *)
+(*v8.5 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 5783e43..2a65c4f 100644
--- a/mathcomp/discrete/fintype.v
+++ b/mathcomp/discrete/fintype.v
@@ -1,5 +1,5 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-(*v8.5 From mathcomp.ssreflect  *)
+(*v8.5 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 c22fa67..d16f43d 100644
--- a/mathcomp/discrete/generic_quotient.v
+++ b/mathcomp/discrete/generic_quotient.v
@@ -1,6 +1,6 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
 (* -*- coding : utf-8 -*- *)
-(*v8.5 From mathcomp.ssreflect  *)
+(*v8.5 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 85746a4..d5e3864 100644
--- a/mathcomp/discrete/path.v
+++ b/mathcomp/discrete/path.v
@@ -1,5 +1,5 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-(*v8.5 From mathcomp.ssreflect  *)
+(*v8.5 From mathcomp.ssreflect   *)
 Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
 
 (******************************************************************************)
diff --git a/mathcomp/discrete/prime.v b/mathcomp/discrete/prime.v
index 77edad1..fde2309 100644
--- a/mathcomp/discrete/prime.v
+++ b/mathcomp/discrete/prime.v
@@ -1,5 +1,5 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-(*v8.5 From mathcomp.ssreflect  *)
+(*v8.5 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 f746dd1..6847df4 100644
--- a/mathcomp/discrete/tuple.v
+++ b/mathcomp/discrete/tuple.v
@@ -1,5 +1,5 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-(*v8.5 From mathcomp.ssreflect  *)
+(*v8.5 From mathcomp.ssreflect   *)
 Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
 Require Import choice fintype.