diff options
| -rw-r--r-- | mathcomp/ssreflect/order.v | 26 |
1 files changed, 6 insertions, 20 deletions
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index d6202c3..5836483 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -1,27 +1,10 @@ -(*************************************************************************) -(* Copyright (C) 2012 - 2016 (Draft) *) -(* C. Cohen *) -(* Based on prior works by *) -(* D. Dreyer, G. Gonthier, A. Nanevski, P-Y Strub, B. Ziliani *) -(* *) -(* This program is free software: you can redistribute it and/or modify *) -(* it under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 3 of the License, or *) -(* (at your option) any later version. *) -(* *) -(* This program is distributed in the hope that it will be useful, *) -(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) -(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) -(* GNU General Public License for more details. *) -(* *) -(* You should have received a copy of the GNU General Public License *) -(* along with this program. If not, see <http://www.gnu.org/licenses/>. *) -(*************************************************************************) +(* (c) Copyright 2006-2019 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) From mathcomp Require Import ssreflect ssrbool eqtype ssrfun ssrnat choice seq. From mathcomp Require Import fintype tuple bigop path finset. (******************************************************************************) -(* This files definies a ordered and decidable relations on a type as *) +(* This files defines a ordered and decidable relations on a type as *) (* canonical structure. One need to import some of the following modules to *) (* get the definitions, notations, and theory of such relations. *) (* Order.Def: definitions of basic operations. *) @@ -113,6 +96,9 @@ From mathcomp Require Import fintype tuple bigop path finset. (* leP ltP ltgtP are the three main lemmas for case analysis. *) (* *) (* We also provide specialized version of some theorems from path.v. *) +(* *) +(* This file is based on prior works by *) +(* D. Dreyer, G. Gonthier, A. Nanevski, P-Y Strub, B. Ziliani *) (******************************************************************************) Set Implicit Arguments. |