diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Lists/SetoidList.v | 1 | ||||
| -rw-r--r-- | theories/Logic/ClassicalUniqueChoice.v | 4 | ||||
| -rw-r--r-- | theories/MSets/MSetGenTree.v | 3 | ||||
| -rw-r--r-- | theories/Reals/RIneq.v | 2 | ||||
| -rw-r--r-- | theories/Sorting/Sorted.v | 2 |
5 files changed, 6 insertions, 6 deletions
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index d75eb384f6..ba62fa7fd5 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -125,7 +125,6 @@ Proof. intros x y z H; revert z; induction H; auto. inversion 1; subst; auto. invlist eqlistA; eauto with *. Qed. - (** Moreover, [eqlistA] implies [equivlistA]. A reverse result will be proved later for sorted list without duplicates. *) diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v index 4a4fc23f94..76f8a55a42 100644 --- a/theories/Logic/ClassicalUniqueChoice.v +++ b/theories/Logic/ClassicalUniqueChoice.v @@ -42,8 +42,8 @@ intros A B. apply (dependent_unique_choice A (fun _ => B)). Qed. -(** The following proof comes from [[ChicliPottierSimpson02]] *) +(** The following proof comes from [[ChicliPottierSimpson02]] *) Require Import Setoid. Theorem classic_set_in_prop_context : @@ -78,7 +78,7 @@ destruct (f P). right. destruct HfP as [[_ Hfalse]| [Hna _]]. discriminate. - assumption. + assumption. Qed. Corollary not_not_classic_set : diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index 3142d97ca9..6164e6e93e 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -962,7 +962,8 @@ Proof. firstorder. Qed. Lemma eq_Leq : forall s s', eq s s' <-> L.eq (elements s) (elements s'). Proof. unfold eq, Equal, L.eq; intros. - setoid_rewrite elements_spec1; firstorder. + do 2 setoid_rewrite elements_spec1. (*FIXME due to regression in rewrite *) + firstorder. Qed. Definition lt (s1 s2 : tree) : Prop := diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index b444d443d0..acc9fd5d64 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -812,7 +812,7 @@ Hint Resolve Rinv_involutive: real. Lemma Rinv_mult_distr : forall r1 r2, r1 <> 0 -> r2 <> 0 -> / (r1 * r2) = / r1 * / r2. Proof. - intros; field; auto. + intros; field; auto. Qed. (*********) diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v index a89b90238e..5b52c6ec9b 100644 --- a/theories/Sorting/Sorted.v +++ b/theories/Sorting/Sorted.v @@ -69,7 +69,7 @@ Section defs. (forall a l, Sorted l -> P l -> HdRel a l -> P (a :: l)) -> forall l:list A, Sorted l -> P l. Proof. - induction l; firstorder using Sorted_inv. + induction l. firstorder using Sorted_inv. firstorder using Sorted_inv. Qed. Lemma Sorted_LocallySorted_iff : forall l, Sorted l <-> LocallySorted l. |