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.
math-comp · Apr 3, 2015 · abe2354 · abe2354
1 parent 9fa572c
commit abe2354
Show file tree

Hide file tree

Showing 13 changed files with 19 additions and 12 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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.