diff options
Diffstat (limited to 'theories/FSets/FMapPositive.v')
| -rw-r--r-- | theories/FSets/FMapPositive.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index e5133f66b2..342a51b39b 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -476,8 +476,8 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. unfold elements. intros m; set (p:=1); clearbody p; revert m p. induction m; simpl; auto; intros. - rewrite (IHm1 (append p 2)), (IHm2 (append p 3)); auto. - destruct o; rewrite app_length; simpl; omega. + rewrite (IHm1 (append p 2)), (IHm2 (append p 3)). + destruct o; rewrite app_length; simpl; auto. Qed. End CompcertSpec. |