diff options
| author |  Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
| commit | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch) | |
| tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /theories/FSets/FMapPositive.v | |
| parent | 6e34b272d789455a9be589e27ad3a998cf25496b (diff) | |
| parent | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff) | |
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to 'theories/FSets/FMapPositive.v')
| -rw-r--r-- | theories/FSets/FMapPositive.v | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index 30bce2db..c59f7c22 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -6,14 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: FMapPositive.v 13297 2010-07-19 23:32:42Z letouzey $ *) - (** * FMapPositive : an implementation of FMapInterface for [positive] keys. *) Require Import Bool ZArith OrderedType OrderedTypeEx FMapInterface. Set Implicit Arguments. -Open Local Scope positive_scope. +Local Open Scope positive_scope. Local Unset Elimination Schemes. Local Unset Case Analysis Schemes. @@ -86,7 +84,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Section A. Variable A:Type. - Implicit Arguments Leaf [A]. + Arguments Leaf [A]. Definition empty : t A := Leaf. @@ -496,9 +494,9 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Definition lt_key (p p':positive*A) := E.lt (fst p) (fst p'). - Global Instance eqk_equiv : Equivalence eq_key. - Global Instance eqke_equiv : Equivalence eq_key_elt. - Global Instance ltk_strorder : StrictOrder lt_key. + Global Program Instance eqk_equiv : Equivalence eq_key. + Global Program Instance eqke_equiv : Equivalence eq_key_elt. + Global Program Instance ltk_strorder : StrictOrder lt_key. Lemma mem_find : forall m x, mem x m = match find x m with None => false | _ => true end. @@ -816,7 +814,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Variable A B C : Type. Variable f : option A -> option B -> option C. - Implicit Arguments Leaf [A]. + Arguments Leaf [A]. Fixpoint xmap2_l (m : t A) : t C := match m with |