diff options
Diffstat (limited to 'theories/FSets')
-rw-r--r-- | theories/FSets/FSetBridge.v | 4 | ||||
-rw-r--r-- | theories/FSets/FSetEqProperties.v | 8 | ||||
-rw-r--r-- | theories/FSets/FSetFacts.v | 6 | ||||
-rw-r--r-- | theories/FSets/FSetProperties.v | 2 |
4 files changed, 9 insertions, 11 deletions
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v index 25ce5577e..f0a588379 100644 --- a/theories/FSets/FSetBridge.v +++ b/theories/FSets/FSetBridge.v @@ -165,7 +165,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. case (for_all (fdec Pdec) s); unfold For_all in |- *; [ left | right ]; intros. assert (compat_bool E.eq (fdec Pdec)); auto. - generalize (H0 H3 (refl_equal _) _ H2). + generalize (H0 H3 Logic.eq_refl _ H2). unfold fdec in |- *. case (Pdec x); intuition. inversion H4. @@ -230,7 +230,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. unfold fdec in |- *; case (Pdec x); intuition. change ((fun x => negb (fdec Pdec x)) x = true) in |- *. apply (filter_2 (s:=s) (x:=x)); auto. - set (b := fdec Pdec x) in *; generalize (refl_equal b); + set (b := fdec Pdec x) in *; generalize (Logic.eq_refl b); pattern b at -1 in |- *; case b; unfold b in |- *; [ left | right ]. elim (H4 x); intros _ B; apply B; auto with set. diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v index 755bc7dd0..ac495c040 100644 --- a/theories/FSets/FSetEqProperties.v +++ b/theories/FSets/FSetEqProperties.v @@ -206,7 +206,7 @@ intros. generalize (@choose_1 s) (@choose_2 s). destruct (choose s);intros. exists e;auto with set. -generalize (H1 (refl_equal None)); clear H1. +generalize (H1 Logic.eq_refl); clear H1. intros; rewrite (is_empty_1 H1) in H; discriminate. Qed. @@ -631,7 +631,7 @@ destruct (choose (filter f s)). intros H0 _; apply exists_1; auto. exists e; generalize (H0 e); rewrite filter_iff; auto. intros _ H0. -rewrite (is_empty_1 (H0 (refl_equal None))) in H; auto; discriminate. +rewrite (is_empty_1 (H0 Logic.eq_refl)) in H; auto; discriminate. Qed. Lemma partition_filter_1: @@ -881,8 +881,8 @@ generalize (@add_filter_1 f Hf s0 (add x s0) x) (@add_filter_2 f Hf s0 (add x s0 assert (~ In x (filter f s0)). intro H1; rewrite (mem_1 (filter_1 Hf H1)) in H; discriminate H. case (f x); simpl; intros. -rewrite (MP.cardinal_2 H1 (H2 (refl_equal true) (MP.Add_add s0 x))); auto. -rewrite <- (MP.Equal_cardinal (H3 (refl_equal false) (MP.Add_add s0 x))); auto. +rewrite (MP.cardinal_2 H1 (H2 Logic.eq_refl (MP.Add_add s0 x))); auto. +rewrite <- (MP.Equal_cardinal (H3 Logic.eq_refl (MP.Add_add s0 x))); auto. intros; rewrite fold_empty;auto. rewrite MP.cardinal_1; auto. unfold Empty; intros. diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v index f473b3342..b240ede4d 100644 --- a/theories/FSets/FSetFacts.v +++ b/theories/FSets/FSetFacts.v @@ -315,11 +315,11 @@ symmetry. rewrite <- H1; intros a Ha. rewrite <- (H a) in Ha. destruct H0 as (_,H0). -exact (H0 (refl_equal true) _ Ha). +exact (H0 Logic.eq_refl _ Ha). rewrite <- H0; intros a Ha. rewrite (H a) in Ha. destruct H1 as (_,H1). -exact (H1 (refl_equal true) _ Ha). +exact (H1 Logic.eq_refl _ Ha). Qed. Instance Empty_m : Proper (Equal ==> iff) Empty. @@ -489,5 +489,3 @@ End WFacts_fun. Module WFacts (M:WS) := WFacts_fun M.E M. Module Facts := WFacts. - - diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v index 8651a96f7..25b042ca9 100644 --- a/theories/FSets/FSetProperties.v +++ b/theories/FSets/FSetProperties.v @@ -823,7 +823,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). rewrite (inter_subset_equal H). generalize (@cardinal_inv_1 (diff s' s)). destruct (cardinal (diff s' s)). - intro H2; destruct (H2 (refl_equal _) x). + intro H2; destruct (H2 Logic.eq_refl x). set_iff; auto. intros _. change (0 + cardinal s < S n + cardinal s). |