diff options
Diffstat (limited to 'mathcomp')
49 files changed, 112 insertions, 161 deletions
diff --git a/mathcomp/algebra/Makefile b/mathcomp/algebra/Makefile index ead5950..e872352 100644 --- a/mathcomp/algebra/Makefile +++ b/mathcomp/algebra/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/algebra/cyclic.v b/mathcomp/algebra/cyclic.v index caeb57f..4365406 100644 --- a/mathcomp/algebra/cyclic.v +++ b/mathcomp/algebra/cyclic.v @@ -1,9 +1,10 @@ (* (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 prime finset. -(*v8.5 From mathcomp.fingroup *) +From mathcomp.fingroup Require Import fingroup morphism perm automorphism quotient gproduct. Require Import ssralg finalg zmodp poly. diff --git a/mathcomp/algebra/finalg.v b/mathcomp/algebra/finalg.v index d364fc9..13daa31 100644 --- a/mathcomp/algebra/finalg.v +++ b/mathcomp/algebra/finalg.v @@ -1,9 +1,10 @@ (* (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 choice fintype finset. -(*v8.5 From mathcomp.fingroup *) +From mathcomp.fingroup Require Import fingroup morphism perm action. Require Import ssralg. diff --git a/mathcomp/algebra/fraction.v b/mathcomp/algebra/fraction.v index 446248f..9ce2718 100644 --- a/mathcomp/algebra/fraction.v +++ b/mathcomp/algebra/fraction.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 tuple bigop generic_quotient. Require Import ssralg poly polydiv. diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index bfd4b13..cdfde3c 100644 --- a/mathcomp/algebra/intdiv.v +++ b/mathcomp/algebra/intdiv.v @@ -1,9 +1,10 @@ (* (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 path div choice fintype tuple finfun bigop prime. -(*v8.5 From mathcomp.fingroup *) +From mathcomp.fingroup Require Import perm. Require Import ssralg poly ssrnum ssrint rat. Require Import polydiv finalg zmodp matrix mxalgebra vector. diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v index 7bde270..bed19fa 100644 --- a/mathcomp/algebra/interval.v +++ b/mathcomp/algebra/interval.v @@ -1,9 +1,10 @@ (* (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 bigop finset. -(*v8.5 From mathcomp.fingroup *) +From mathcomp.fingroup Require Import fingroup. Require Import ssralg zmodp ssrint ssrnum. diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index e67008d..9339e67 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -1,9 +1,10 @@ (* (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 finfun bigop prime binomial finset. -(*v8.5 From mathcomp.fingroup *) +From mathcomp.fingroup Require Import fingroup perm. Require Import ssralg finalg zmodp. diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index 833a229..cb1717c 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -1,9 +1,10 @@ (* (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 finfun bigop prime binomial finset. -(*v8.5 From mathcomp.fingroup *) +From mathcomp.fingroup Require Import fingroup perm. Require Import ssralg finalg zmodp matrix. diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index 8a0b519..bc5a998 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -1,9 +1,10 @@ (* (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 fintype tuple finfun bigop. -(*v8.5 From mathcomp.fingroup *) +From mathcomp.fingroup Require Import fingroup perm. Require Import ssralg zmodp matrix mxalgebra poly polydiv. diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index e473f2d..2757b30 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.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 binomial. Require Import ssralg. diff --git a/mathcomp/algebra/polyXY.v b/mathcomp/algebra/polyXY.v index 5abc40d..d79b2bf 100644 --- a/mathcomp/algebra/polyXY.v +++ b/mathcomp/algebra/polyXY.v @@ -1,9 +1,10 @@ (* (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 choice div fintype tuple finfun bigop binomial. -(*v8.5 From mathcomp.fingroup *) +From mathcomp.fingroup Require Import fingroup perm. Require Import ssralg zmodp matrix mxalgebra poly polydiv mxpoly. diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v index fa3a132..5910586 100644 --- a/mathcomp/algebra/polydiv.v +++ b/mathcomp/algebra/polydiv.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 bigop choice fintype. Require Import ssralg poly. diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v index 342eead..398d8de 100644 --- a/mathcomp/algebra/rat.v +++ b/mathcomp/algebra/rat.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 bigop. Require Import ssralg ssrnum ssrint. diff --git a/mathcomp/algebra/ring_quotient.v b/mathcomp/algebra/ring_quotient.v index 6f2a2f5..ea41744 100644 --- a/mathcomp/algebra/ring_quotient.v +++ b/mathcomp/algebra/ring_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 ssrnat eqtype seq. -(*v8.5 From mathcomp.discrete *) +From mathcomp.discrete Require Import choice generic_quotient. Require Import ssralg. diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 3627447..820a4b9 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.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 finfun bigop prime binomial. (******************************************************************************) diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index 3281c44..48c78dd 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.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 choice fintype finfun bigop. Require Import ssralg ssrnum poly. diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 19d4c31..aecb910 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -1,9 +1,10 @@ (* (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 bigop finset. -(*v8.5 From mathcomp.fingroup *) +From mathcomp.fingroup Require Import fingroup. Require Import ssralg zmodp poly. diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index 0d4ace0..01f2f53 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.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 choice fintype bigop finfun tuple. Require Import ssralg matrix mxalgebra zmodp. diff --git a/mathcomp/algebra/zmodp.v b/mathcomp/algebra/zmodp.v index 614bf10..9dd3ff5 100644 --- a/mathcomp/algebra/zmodp.v +++ b/mathcomp/algebra/zmodp.v @@ -1,9 +1,10 @@ (* (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 fintype bigop finset prime. -(*v8.5 From mathcomp.fingroup *) +From mathcomp.fingroup Require Import fingroup. Require Import ssralg finalg. diff --git a/mathcomp/all/Makefile b/mathcomp/all/Makefile index ead5950..e872352 100644 --- a/mathcomp/all/Makefile +++ b/mathcomp/all/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/attic/Makefile b/mathcomp/attic/Makefile index ead5950..e872352 100644 --- a/mathcomp/attic/Makefile +++ b/mathcomp/attic/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/character/Makefile b/mathcomp/character/Makefile index ead5950..e872352 100644 --- a/mathcomp/character/Makefile +++ b/mathcomp/character/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/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. diff --git a/mathcomp/field/Makefile b/mathcomp/field/Makefile index ead5950..e872352 100644 --- a/mathcomp/field/Makefile +++ b/mathcomp/field/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/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. diff --git a/mathcomp/odd_order/Makefile b/mathcomp/odd_order/Makefile index ead5950..e872352 100644 --- a/mathcomp/odd_order/Makefile +++ b/mathcomp/odd_order/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/real_closed/Makefile b/mathcomp/real_closed/Makefile index ead5950..e872352 100644 --- a/mathcomp/real_closed/Makefile +++ b/mathcomp/real_closed/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/solvable/Makefile b/mathcomp/solvable/Makefile index ead5950..e872352 100644 --- a/mathcomp/solvable/Makefile +++ b/mathcomp/solvable/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/ssrtest/Makefile b/mathcomp/ssrtest/Makefile index 3614d33..4bcf4fb 100644 --- a/mathcomp/ssrtest/Makefile +++ b/mathcomp/ssrtest/Makefile @@ -7,12 +7,6 @@ MAKEFLAGS := -r COQMAKEFILE := Makefile.coq COQMAKE := +$(MAKE) -f $(COQMAKEFILE) -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 - all: $(COQMAKEFILE) $(COQMAKE) all @@ -29,5 +23,4 @@ tags: install: %: Makefile.coq - sed -i -e "s/^(\*$(VERSION_Coq) *\(.*\) *\*)/\1/" *.v $(COQMAKE) $@ |