diff options
| author | Cyril Cohen | 2019-05-15 11:42:43 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2019-12-11 14:25:52 +0100 |
| commit | 6d34f29cf906b6672925ee3abd4e54b59eea784f (patch) | |
| tree | 9ee30f84b3ca84f2d652611a54c2d88239fe5208 /mathcomp/ssreflect/order.v | |
| parent | fbf0b7568b8d6231671954cba8bcae4120e591cc (diff) | |
Changing license
Diffstat (limited to 'mathcomp/ssreflect/order.v')
| -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. |