aboutsummaryrefslogtreecommitdiff
path: root/theories/FSets
diff options
context:
space:
mode:
Diffstat (limited to 'theories/FSets')
-rw-r--r--theories/FSets/FMapAVL.v2
-rw-r--r--theories/FSets/FMapFacts.v6
-rw-r--r--theories/FSets/FMapFullAVL.v2
-rw-r--r--theories/FSets/FMapInterface.v4
-rw-r--r--theories/FSets/FMapList.v2
-rw-r--r--theories/FSets/FMapPositive.v10
-rw-r--r--theories/FSets/FMapWeakList.v2
-rw-r--r--theories/FSets/FMaps.v2
-rw-r--r--theories/FSets/FSetAVL.v2
-rw-r--r--theories/FSets/FSetBridge.v2
-rw-r--r--theories/FSets/FSetCompat.v2
-rw-r--r--theories/FSets/FSetDecide.v4
-rw-r--r--theories/FSets/FSetEqProperties.v2
-rw-r--r--theories/FSets/FSetFacts.v2
-rw-r--r--theories/FSets/FSetInterface.v2
-rw-r--r--theories/FSets/FSetList.v2
-rw-r--r--theories/FSets/FSetPositive.v30
-rw-r--r--theories/FSets/FSetProperties.v2
-rw-r--r--theories/FSets/FSetToFiniteSet.v2
-rw-r--r--theories/FSets/FSetWeakList.v2
-rw-r--r--theories/FSets/FSets.v2
21 files changed, 43 insertions, 43 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 63f907e567..801be79ba4 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index e68bc5930d..1a531542cc 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -1988,7 +1988,7 @@ Module OrdProperties (M:S).
simpl; intros; try discriminate.
intros.
destruct a; destruct l; simpl in *.
- injection H as -> ->.
+ injection H as [= -> ->].
inversion_clear H1.
red in H; simpl in *; intuition.
elim H0; eauto.
@@ -2052,7 +2052,7 @@ Module OrdProperties (M:S).
generalize (elements_3 m).
destruct (elements m).
try discriminate.
- destruct p; injection H as -> ->; intros H4.
+ destruct p; injection H as [= -> ->]; intros H4.
inversion_clear H1 as [? ? H2|? ? H2].
red in H2; destruct H2; simpl in *; ME.order.
inversion_clear H4. rename H1 into H3.
diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v
index b23885154b..8ca9401a06 100644
--- a/theories/FSets/FMapFullAVL.v
+++ b/theories/FSets/FMapFullAVL.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v
index 8970529103..a6ef26de0e 100644
--- a/theories/FSets/FMapInterface.v
+++ b/theories/FSets/FMapInterface.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -192,7 +192,7 @@ Module Type WSfun (E : DecidableType).
(** Equality of maps *)
(** Caveat: there are at least three distinct equality predicates on maps.
- - The simpliest (and maybe most natural) way is to consider keys up to
+ - The simplest (and maybe most natural) way is to consider keys up to
their equivalence [E.eq], but elements up to Leibniz equality, in
the spirit of [eq_key_elt] above. This leads to predicate [Equal].
- Unfortunately, this [Equal] predicate can't be used to describe
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index 335fdc3232..2af6e5c6a4 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index b47c99244b..e5133f66b2 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -277,7 +277,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
rewrite append_assoc_1; apply in_or_app; right; apply in_cons;
apply IHm2; auto.
rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto.
- rewrite append_neutral_r; apply in_or_app; injection H as ->;
+ rewrite append_neutral_r; apply in_or_app; injection H as [= ->];
right; apply in_eq.
rewrite append_assoc_1; apply in_or_app; right; apply IHm2; auto.
rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto.
@@ -318,7 +318,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
apply in_or_app.
left; apply IHm1; auto.
right; destruct (in_inv H0).
- injection H1 as -> ->; apply in_eq.
+ injection H1 as [= -> ->]; apply in_eq.
apply in_cons; apply IHm2; auto.
left; apply IHm1; auto.
right; apply IHm2; auto.
@@ -349,7 +349,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
apply in_or_app.
left; apply IHm1; auto.
right; destruct (in_inv H0).
- injection H1 as -> ->; apply in_eq.
+ injection H1 as [= -> ->]; apply in_eq.
apply in_cons; apply IHm2; auto.
left; apply IHm1; auto.
right; apply IHm2; auto.
@@ -692,7 +692,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
destruct y2; destruct y0; compute in Hy2; destruct Hy2; subst.
red; red; simpl.
destruct H0.
- injection H0 as H0 _; subst.
+ injection H0 as [= H0 _]; subst.
eapply xelements_bits_lt_1; eauto.
apply E.bits_lt_trans with p.
eapply xelements_bits_lt_1; eauto.
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index 12550ddf9a..0c04437581 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/theories/FSets/FMaps.v b/theories/FSets/FMaps.v
index ec50763589..1eefb1c0ad 100644
--- a/theories/FSets/FMaps.v
+++ b/theories/FSets/FMaps.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index dcaea894eb..f466052b98 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -1,7 +1,7 @@
(* -*- coding: utf-8 -*- *)
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index 3952c28061..6e08c38a49 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/theories/FSets/FSetCompat.v b/theories/FSets/FSetCompat.v
index 736c85dada..fa275bc48f 100644
--- a/theories/FSets/FSetCompat.v
+++ b/theories/FSets/FSetCompat.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index 83bb07ffb6..b795ed42e3 100644
--- a/theories/FSets/FSetDecide.v
+++ b/theories/FSets/FSetDecide.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -240,7 +240,7 @@ the above form:
True.
Proof.
intros. push not in *.
- (* note that ~(R->P) remains (since R isnt decidable) *)
+ (* note that ~(R->P) remains (since R isn't decidable) *)
tauto.
Qed.
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index 3f8840529e..da504259f5 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v
index f4d281e937..8c96bec647 100644
--- a/theories/FSets/FSetFacts.v
+++ b/theories/FSets/FSetFacts.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index fa7f1c5f4e..141935c31a 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/theories/FSets/FSetList.v b/theories/FSets/FSetList.v
index 2036d360aa..916ba4ff66 100644
--- a/theories/FSets/FSetList.v
+++ b/theories/FSets/FSetList.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/theories/FSets/FSetPositive.v b/theories/FSets/FSetPositive.v
index 8a93f38164..35e97a47c1 100644
--- a/theories/FSets/FSetPositive.v
+++ b/theories/FSets/FSetPositive.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -1009,10 +1009,10 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
destruct o.
intros x H. injection H; intros; subst. reflexivity.
revert IHl. case choose.
- intros p Hp x H. injection H as <-. apply Hp.
+ intros p Hp x [= <-]. apply Hp.
reflexivity.
intros _ x. revert IHr. case choose.
- intros p Hp H. injection H as <-. apply Hp.
+ intros p Hp [= <-]. apply Hp.
reflexivity.
intros. discriminate.
Qed.
@@ -1068,11 +1068,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
induction s as [| l IHl o r IHr]; simpl.
intros. discriminate.
intros x. destruct (min_elt l); intros.
- injection H as <-. apply IHl. reflexivity.
+ injection H as [= <-]. apply IHl. reflexivity.
destruct o; simpl.
- injection H as <-. reflexivity.
+ injection H as [= <-]. reflexivity.
destruct (min_elt r); simpl in *.
- injection H as <-. apply IHr. reflexivity.
+ injection H as [= <-]. apply IHr. reflexivity.
discriminate.
Qed.
@@ -1096,15 +1096,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
induction s as [|l IHl o r IHr]; intros x y H H'.
discriminate.
simpl in H. case_eq (min_elt l).
- intros p Hp. rewrite Hp in H. injection H as <-.
+ intros p Hp. rewrite Hp in H. injection H as [= <-].
destruct y as [z|z|]; simpl; intro; trivial. apply (IHl p z); trivial.
intro Hp; rewrite Hp in H. apply min_elt_3 in Hp.
destruct o.
- injection H as <-. intros Hl.
+ injection H as [= <-]. intros Hl.
destruct y as [z|z|]; simpl; trivial. elim (Hp _ H').
destruct (min_elt r).
- injection H as <-.
+ injection H as [= <-].
destruct y as [z|z|].
apply (IHr e z); trivial.
elim (Hp _ H').
@@ -1121,11 +1121,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
induction s as [| l IHl o r IHr]; simpl.
intros. discriminate.
intros x. destruct (max_elt r); intros.
- injection H as <-. apply IHr. reflexivity.
+ injection H as [= <-]. apply IHr. reflexivity.
destruct o; simpl.
- injection H as <-. reflexivity.
+ injection H as [= <-]. reflexivity.
destruct (max_elt l); simpl in *.
- injection H as <-. apply IHl. reflexivity.
+ injection H as [= <-]. apply IHl. reflexivity.
discriminate.
Qed.
@@ -1149,15 +1149,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
induction s as [|l IHl o r IHr]; intros x y H H'.
discriminate.
simpl in H. case_eq (max_elt r).
- intros p Hp. rewrite Hp in H. injection H as <-.
+ intros p Hp. rewrite Hp in H. injection H as [= <-].
destruct y as [z|z|]; simpl; intro; trivial. apply (IHr p z); trivial.
intro Hp; rewrite Hp in H. apply max_elt_3 in Hp.
destruct o.
- injection H as <-. intros Hl.
+ injection H as [= <-]. intros Hl.
destruct y as [z|z|]; simpl; trivial. elim (Hp _ H').
destruct (max_elt l).
- injection H as <-.
+ injection H as [= <-].
destruct y as [z|z|].
elim (Hp _ H').
apply (IHl e z); trivial.
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index 6b6546f82d..c6b2e0a09d 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/theories/FSets/FSetToFiniteSet.v b/theories/FSets/FSetToFiniteSet.v
index f8d13ed2ba..d64ee9fd98 100644
--- a/theories/FSets/FSetToFiniteSet.v
+++ b/theories/FSets/FSetToFiniteSet.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v
index 1dacd05681..54cfc6e2b0 100644
--- a/theories/FSets/FSetWeakList.v
+++ b/theories/FSets/FSetWeakList.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/theories/FSets/FSets.v b/theories/FSets/FSets.v
index 7e9e7aae7e..07a06a923d 100644
--- a/theories/FSets/FSets.v
+++ b/theories/FSets/FSets.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 09:10:17 +0000