diff options
| -rw-r--r-- | mathcomp/discrete/all.v | 1 | ||||
| -rw-r--r-- | mathcomp/discrete/bigop.v | 5 | ||||
| -rw-r--r-- | mathcomp/discrete/binomial.v | 5 | ||||
| -rw-r--r-- | mathcomp/discrete/choice.v | 1 | ||||
| -rw-r--r-- | mathcomp/discrete/div.v | 1 | ||||
| -rw-r--r-- | mathcomp/discrete/finfun.v | 4 | ||||
| -rw-r--r-- | mathcomp/discrete/fingraph.v | 4 | ||||
| -rw-r--r-- | mathcomp/discrete/finset.v | 5 | ||||
| -rw-r--r-- | mathcomp/discrete/fintype.v | 4 | ||||
| -rw-r--r-- | mathcomp/discrete/generic_quotient.v | 5 | ||||
| -rw-r--r-- | mathcomp/discrete/path.v | 1 | ||||
| -rw-r--r-- | mathcomp/discrete/prime.v | 5 | ||||
| -rw-r--r-- | mathcomp/discrete/tuple.v | 4 |
13 files changed, 30 insertions, 15 deletions
diff --git a/mathcomp/discrete/all.v b/mathcomp/discrete/all.v index 8412bdb..dfa8536 100644 --- a/mathcomp/discrete/all.v +++ b/mathcomp/discrete/all.v @@ -1,4 +1,3 @@ -Require Export mathcomp.ssreflect.all. Require Export choice. Require Export path. Require Export div. diff --git a/mathcomp/discrete/bigop.v b/mathcomp/discrete/bigop.v index 88bf4d2..b6d77ec 100644 --- a/mathcomp/discrete/bigop.v +++ b/mathcomp/discrete/bigop.v @@ -1,6 +1,7 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path div fintype. -Require Import tuple finfun. +(*v8.5 From mathcomp.ssreflect *) +Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. +Require Import path div fintype tuple finfun. (******************************************************************************) (* This file provides a generic definition for iterating an operator over a *) diff --git a/mathcomp/discrete/binomial.v b/mathcomp/discrete/binomial.v index 756a8f9..5656b30 100644 --- a/mathcomp/discrete/binomial.v +++ b/mathcomp/discrete/binomial.v @@ -1,6 +1,7 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path div. -Require Import fintype tuple finfun bigop prime finset. +(*v8.5 From mathcomp.ssreflect *) +Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +Require Import path div fintype tuple finfun bigop prime finset. (******************************************************************************) (* This files contains the definition of: *) diff --git a/mathcomp/discrete/choice.v b/mathcomp/discrete/choice.v index 96b549c..cfd0b58 100644 --- a/mathcomp/discrete/choice.v +++ b/mathcomp/discrete/choice.v @@ -1,4 +1,5 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +(*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 d06a8e3..0d94936 100644 --- a/mathcomp/discrete/div.v +++ b/mathcomp/discrete/div.v @@ -1,4 +1,5 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +(*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 f880260..e6c6afc 100644 --- a/mathcomp/discrete/finfun.v +++ b/mathcomp/discrete/finfun.v @@ -1,5 +1,7 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple. +(*v8.5 From mathcomp.ssreflect *) +Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +Require Import choice fintype tuple. (******************************************************************************) (* This file implements a type for functions with a finite domain: *) diff --git a/mathcomp/discrete/fingraph.v b/mathcomp/discrete/fingraph.v index 403d1ca..d445510 100644 --- a/mathcomp/discrete/fingraph.v +++ b/mathcomp/discrete/fingraph.v @@ -1,5 +1,7 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path fintype. +(*v8.5 From mathcomp.ssreflect *) +Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. +Require Import path fintype. (******************************************************************************) (* This file develops the theory of finite graphs represented by an "edge" *) diff --git a/mathcomp/discrete/finset.v b/mathcomp/discrete/finset.v index 54dacc0..5067701 100644 --- a/mathcomp/discrete/finset.v +++ b/mathcomp/discrete/finset.v @@ -1,6 +1,7 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import ssreflect ssrbool ssrfun eqtype ssrnat div seq choice fintype. -Require Import finfun bigop. +(*v8.5 From mathcomp.ssreflect *) +Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. +Require Import bigop choice fintype div finfun. (******************************************************************************) (* This file defines a type for sets over a finite Type, similar to the type *) diff --git a/mathcomp/discrete/fintype.v b/mathcomp/discrete/fintype.v index 63d5e84..5783e43 100644 --- a/mathcomp/discrete/fintype.v +++ b/mathcomp/discrete/fintype.v @@ -1,5 +1,7 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice. +(*v8.5 From mathcomp.ssreflect *) +Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +Require Import choice. (******************************************************************************) (* The Finite interface describes Types with finitely many elements, *) diff --git a/mathcomp/discrete/generic_quotient.v b/mathcomp/discrete/generic_quotient.v index 1d9bd56..c22fa67 100644 --- a/mathcomp/discrete/generic_quotient.v +++ b/mathcomp/discrete/generic_quotient.v @@ -1,7 +1,8 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) (* -*- coding : utf-8 -*- *) - -Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq fintype. +(*v8.5 From mathcomp.ssreflect *) +Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +Require Import choice fintype. (*****************************************************************************) (* Provided a base type T, this files defines an interface for quotients Q *) diff --git a/mathcomp/discrete/path.v b/mathcomp/discrete/path.v index 804e673..85746a4 100644 --- a/mathcomp/discrete/path.v +++ b/mathcomp/discrete/path.v @@ -1,4 +1,5 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +(*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 fa39012..77edad1 100644 --- a/mathcomp/discrete/prime.v +++ b/mathcomp/discrete/prime.v @@ -1,6 +1,7 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path fintype. -Require Import div bigop. +(*v8.5 From mathcomp.ssreflect *) +Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +Require Import path fintype div bigop. (******************************************************************************) (* This file contains the definitions of: *) diff --git a/mathcomp/discrete/tuple.v b/mathcomp/discrete/tuple.v index ba64bd0..f746dd1 100644 --- a/mathcomp/discrete/tuple.v +++ b/mathcomp/discrete/tuple.v @@ -1,5 +1,7 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype. +(*v8.5 From mathcomp.ssreflect *) +Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +Require Import choice fintype. Set Implicit Arguments. Unset Strict Implicit. |