diff options
Diffstat (limited to 'theories/MSets/MSetGenTree.v')
| -rw-r--r-- | theories/MSets/MSetGenTree.v | 22 |
1 files changed, 12 insertions, 10 deletions
diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index 154c2384..95868861 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -1,17 +1,19 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) (** * MSetGenTree : sets via generic trees This module factorizes common parts in implementations of finite sets as AVL trees and as Red-Black trees. The nodes of the trees defined here include an generic information - parameter, that will be the heigth in AVL trees and the color + parameter, that will be the height in AVL trees and the color in Red-Black trees. Without more details here about these information parameters, trees here are not known to be well-balanced, but simply binary-search-trees. @@ -27,7 +29,7 @@ - min_elt max_elt choose *) -Require Import Orders OrdersFacts MSetInterface PeanoNat. +Require Import FunInd Orders OrdersFacts MSetInterface PeanoNat. Local Open Scope list_scope. Local Open Scope lazy_bool_scope. @@ -1144,4 +1146,4 @@ Proof. apply mindepth_cardinal. Qed. -End Props.
\ No newline at end of file +End Props. |