diff options
| author | Frédéric Besson | 2019-10-22 14:30:51 +0200 |
|---|---|---|
| committer | Frédéric Besson | 2019-10-22 14:30:51 +0200 |
| commit | ac8633ba19a7d8e937bbd6f9b7de2ad82b89f22f (patch) | |
| tree | b6512ba01f5b00fe490fe90b9d848c0d8a4c1f80 /theories/FSets/FMapPositive.v | |
| parent | 487f23187413e6cf6ee117d798a9057d0008aa6a (diff) | |
| parent | 4af9a79457fc265b1696de2b1fa1018ef12c986a (diff) | |
Merge PR #10875: [Stdlib] Remove some uses of the “omega” tactic
Reviewed-by: fajb
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. |