diff options
Diffstat (limited to 'theories/FSets')
| -rw-r--r-- | theories/FSets/FMapPositive.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index a0ecdb756..c9d868c40 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -212,7 +212,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. try rewrite <- (gleaf i); auto; try apply IHi; congruence. Qed. - Lemma rleaf : forall (i : key), remove i (Leaf : t A) = Leaf. + Lemma rleaf : forall (i : key), remove i Leaf = Leaf. Proof. destruct i; simpl; auto. Qed. Theorem grs: |