diff options
Diffstat (limited to 'theories/FSets/FMapFullAVL.v')
| -rw-r--r-- | theories/FSets/FMapFullAVL.v | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v index e1c60351..a7be3232 100644 --- a/theories/FSets/FMapFullAVL.v +++ b/theories/FSets/FMapFullAVL.v @@ -660,7 +660,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: Fixpoint cardinal_e (e:Raw.enumeration D.t) := match e with - | Raw.End => 0%nat + | Raw.End _ => 0%nat | Raw.More _ _ r e => S (Raw.cardinal r + cardinal_e e) end. @@ -674,12 +674,14 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: Definition cardinal_e_2 ee := (cardinal_e (fst ee) + cardinal_e (snd ee))%nat. + Local Unset Keyed Unification. + Function compare_aux (ee:Raw.enumeration D.t * Raw.enumeration D.t) { measure cardinal_e_2 ee } : comparison := match ee with - | (Raw.End, Raw.End) => Eq - | (Raw.End, Raw.More _ _ _ _) => Lt - | (Raw.More _ _ _ _, Raw.End) => Gt + | (Raw.End _, Raw.End _) => Eq + | (Raw.End _, Raw.More _ _ _ _) => Lt + | (Raw.More _ _ _ _, Raw.End _) => Gt | (Raw.More x1 d1 r1 e1, Raw.More x2 d2 r2 e2) => match X.compare x1 x2 with | EQ _ => match D.compare d1 d2 with @@ -726,7 +728,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: intros. assert (H1:=cons_1 m1 (Raw.End _)). assert (H2:=cons_1 m2 (Raw.End _)). - simpl in *; rewrite <- app_nil_end in *; rewrite <-H1,<-H2. + simpl in *; rewrite app_nil_r in *; rewrite <-H1,<-H2. apply (@compare_aux_Cmp (Raw.cons m1 (Raw.End _), Raw.cons m2 (Raw.End _))). Qed. |