From abe2354abf63ad98dbe7e54a34e59e20b38d3d55 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Fri, 3 Apr 2015 17:45:38 +0200
Subject: Makefile, testing for v8.5 and uncommenting stuff

This is a temporary solution, but there is a better one :
one could patch ssreflect.ml4 plugin for v8.4 to interpret
From ... Require Import ... as a simple Require Import.
---
 mathcomp/discrete/Makefile           | 7 +++++++
 mathcomp/discrete/bigop.v            | 2 +-
 mathcomp/discrete/binomial.v         | 2 +-
 mathcomp/discrete/choice.v           | 2 +-
 mathcomp/discrete/div.v              | 2 +-
 mathcomp/discrete/finfun.v           | 2 +-
 mathcomp/discrete/fingraph.v         | 2 +-
 mathcomp/discrete/finset.v           | 2 +-
 mathcomp/discrete/fintype.v          | 2 +-
 mathcomp/discrete/generic_quotient.v | 2 +-
 mathcomp/discrete/path.v             | 2 +-
 mathcomp/discrete/prime.v            | 2 +-
 mathcomp/discrete/tuple.v            | 2 +-
 13 files changed, 19 insertions(+), 12 deletions(-)

(limited to 'mathcomp')

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.
 
-- 
cgit v1.2.3