3 files changed, 6 insertions, 6 deletions
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 99705966..2d5a7983 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -26,7 +26,7 @@ Hint Extern 1 (Equivalence _) => constructor; congruence.
 
 Module WFacts_fun (E:DecidableType)(Import M:WSfun E).
 
-Notation option_map := option_map (compat "8.6").
+Notation option_map := option_map (compat "8.7").
 
 Notation eq_dec := E.eq_dec.
 Definition eqb x y := if eq_dec x y then true else false.
diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v
index 34529678..c0db8646 100644
--- a/theories/FSets/FMapFullAVL.v
+++ b/theories/FSets/FMapFullAVL.v
@@ -27,7 +27,7 @@
 
 *)
 
-Require Import FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL ROmega.
+Require Import FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -39,7 +39,7 @@ Import Raw.Proofs.
 Local Open Scope pair_scope.
 Local Open Scope Int_scope.
 
-Ltac omega_max := i2z_refl; romega with Z.
+Ltac omega_max := i2z_refl; lia.
 
 Section Elt.
 Variable elt : Type.
@@ -697,7 +697,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
   end.
   Proof.
   intros; unfold cardinal_e_2; simpl;
-  abstract (do 2 rewrite cons_cardinal_e; romega with * ).
+  abstract (do 2 rewrite cons_cardinal_e; lia ).
   Defined.
 
   Definition Cmp c :=
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index 56844f47..59b2f789 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -333,7 +333,7 @@ Proof.
 auto with set.
 Qed.
 
-(* caracterisation of [union] via [subset] *)
+(* characterisation of [union] via [subset] *)
 
 Lemma union_subset_1: subset s (union s s')=true.
 Proof.
@@ -408,7 +408,7 @@ intros; apply equal_1; apply inter_add_2.
 rewrite not_mem_iff; auto.
 Qed.
 
-(* caracterisation of [union] via [subset] *)
+(* characterisation of [union] via [subset] *)
 
 Lemma inter_subset_1: subset (inter s s') s=true.
 Proof.