Merge PR #9386: Pass some files to strict focusing mode.

Reviewed-by: Zimmi48
Reviewed-by: herbelin
Reviewed-by: ppedrot

5 files changed, 98 insertions, 83 deletions

diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index 97510578ae..f9ca1bed29 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -164,7 +164,11 @@ Section Relations.
 
   Lemma pointwise_pointwise {B} (R : crelation B) :
     relation_equivalence (pointwise_relation R) (@eq A ==> R).
-  Proof. intros. split. simpl_crelation. firstorder. Qed.
+  Proof.
+    intros. split.
+    - simpl_crelation.
+    - firstorder.
+  Qed.
   
   (** Subcrelations induce a morphism on the identity. *)
   
@@ -265,8 +269,8 @@ Section GenericInstances.
   Next Obligation.
   Proof with auto.
     assert(R x0 x0).
-    transitivity y0... symmetry...
-    transitivity (y x0)...
+    - transitivity y0... symmetry...
+    - transitivity (y x0)...
   Qed.
 
   Unset Strict Universe Declaration.
@@ -339,10 +343,11 @@ Section GenericInstances.
 
   Next Obligation.
   Proof with auto.
-    split. intros ; transitivity x0...
-    intros.
-    transitivity y...
-    symmetry...
+    split.
+    - intros ; transitivity x0...
+    - intros.
+      transitivity y...
+      symmetry...
   Qed.
 
   (** Every Transitive crelation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof to get an [R y z] goal. *)
@@ -364,9 +369,9 @@ Section GenericInstances.
   Next Obligation.
   Proof with auto.
     split ; intros.
-    transitivity x0... transitivity x... symmetry...
+    - transitivity x0... transitivity x... symmetry...
 
-    transitivity y... transitivity y0... symmetry...
+    - transitivity y... transitivity y0... symmetry...
   Qed.
 
   Lemma symmetric_equiv_flip `(Symmetric A R) : relation_equivalence R (flip R).
@@ -397,8 +402,8 @@ Section GenericInstances.
     intros A B R R' HRR' S S' HSS' f g. 
     unfold respectful , relation_equivalence in *; simpl in *.
     split ; intros H x y Hxy.
-    apply (fst (HSS' _ _)). apply H. now apply (snd (HRR' _ _)). 
-    apply (snd (HSS' _ _)). apply H. now apply (fst (HRR' _ _)). 
+    - apply (fst (HSS' _ _)). apply H. now apply (snd (HRR' _ _)).
+    - apply (snd (HSS' _ _)). apply H. now apply (fst (HRR' _ _)).
   Qed.
 
   (** [R] is Reflexive, hence we can build the needed proof. *)
@@ -500,8 +505,8 @@ Instance proper_proper : Proper (relation_equivalence ==> eq ==> iffT) (@Proper
 Proof.
   intros A R R' HRR' x y <-. red in HRR'.
   split ; red ; intros. 
-  now apply (fst (HRR' _ _)). 
-  now apply (snd (HRR' _ _)).
+  - now apply (fst (HRR' _ _)).
+  - now apply (snd (HRR' _ _)).
 Qed.
 
 Ltac proper_reflexive :=
@@ -636,9 +641,9 @@ intros.
 apply proper_sym_arrow_iffT_2; auto with *.
 intros x x' Hx y y' Hy Hr.
 transitivity x.
-generalize (partial_order_equivalence x x'); compute; intuition.
-transitivity y; auto.
-generalize (partial_order_equivalence y y'); compute; intuition.
+- generalize (partial_order_equivalence x x'); compute; intuition.
+- transitivity y; auto.
+  generalize (partial_order_equivalence y y'); compute; intuition.
 Qed.
 
 (** From a [PartialOrder] to the corresponding [StrictOrder]:
@@ -649,13 +654,13 @@ Lemma PartialOrder_StrictOrder `(PartialOrder A eqA R) :
   StrictOrder (relation_conjunction R (complement eqA)).
 Proof.
 split; compute.
-intros x (_,Hx). apply Hx, Equivalence_Reflexive.
-intros x y z (Hxy,Hxy') (Hyz,Hyz'). split.
-apply PreOrder_Transitive with y; assumption.
-intro Hxz.
-apply Hxy'.
-apply partial_order_antisym; auto.
-rewrite Hxz. auto.
+- intros x (_,Hx). apply Hx, Equivalence_Reflexive.
+- intros x y z (Hxy,Hxy') (Hyz,Hyz'). split.
+  + apply PreOrder_Transitive with y; assumption.
+  + intro Hxz.
+    apply Hxy'.
+    apply partial_order_antisym; auto.
+    rewrite Hxz. auto.
 Qed.
 
 (** From a [StrictOrder] to the corresponding [PartialOrder]:
@@ -667,12 +672,12 @@ Lemma StrictOrder_PreOrder
  PreOrder (relation_disjunction R eqA).
 Proof.
 split.
-intros x. right. reflexivity.
-intros x y z [Hxy|Hxy] [Hyz|Hyz].
-left. transitivity y; auto.
-left. rewrite <- Hyz; auto.
-left. rewrite Hxy; auto.
-right. transitivity y; auto.
+- intros x. right. reflexivity.
+- intros x y z [Hxy|Hxy] [Hyz|Hyz].
+  + left. transitivity y; auto.
+  + left. rewrite <- Hyz; auto.
+  + left. rewrite Hxy; auto.
+  + right. transitivity y; auto.
 Qed.
 
 Hint Extern 4 (PreOrder (relation_disjunction _ _)) => 
diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v
index bb873588b1..c014ecc7ab 100644
--- a/theories/Classes/CRelationClasses.v
+++ b/theories/Classes/CRelationClasses.v
@@ -315,9 +315,11 @@ Section Binary.
 
   Global Instance relation_equivalence_equivalence :
     Equivalence relation_equivalence.
-  Proof. split; red; unfold relation_equivalence, iffT. firstorder. 
-    firstorder. 
-    intros. specialize (X x0 y0). specialize (X0 x0 y0). firstorder.
+  Proof.
+    split; red; unfold relation_equivalence, iffT.
+    - firstorder.
+    - firstorder.
+    - intros. specialize (X x0 y0). specialize (X0 x0 y0). firstorder.
   Qed.
     
   Global Instance relation_implication_preorder : PreOrder (@subrelation A).
@@ -342,8 +344,11 @@ Section Binary.
   Qed.
 
   Lemma PartialOrder_inverse `(PartialOrder eqA R) : PartialOrder eqA (flip R).
-  Proof. unfold flip; constructor; unfold flip. intros. apply H. apply symmetry. apply X.
-         unfold relation_conjunction. intros [H1 H2]. apply H. constructor; assumption. Qed.
+  Proof.
+    unfold flip; constructor; unfold flip.
+    - intros. apply H. apply symmetry. apply X.
+    - unfold relation_conjunction. intros [H1 H2]. apply H. constructor; assumption.
+  Qed.
 End Binary.
 
 Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : typeclass_instances.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 001b7dfdfd..a4fa537128 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -260,8 +260,8 @@ Section GenericInstances.
   Next Obligation.
   Proof with auto.
     assert(R x0 x0).
-    transitivity y0... symmetry...
-    transitivity (y x0)... 
+    - transitivity y0... symmetry...
+    - transitivity (y x0)...
   Qed.
 
   (** The complement of a relation conserves its proper elements. *)
@@ -344,10 +344,11 @@ Section GenericInstances.
 
   Next Obligation.
   Proof with auto.
-    split. intros ; transitivity x0...
-    intros.
-    transitivity y...
-    symmetry...
+    split.
+    - intros ; transitivity x0...
+    - intros.
+      transitivity y...
+      symmetry...
   Qed.
 
   (** Every Transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof to get an [R y z] goal. *)
@@ -369,9 +370,9 @@ Section GenericInstances.
   Next Obligation.
   Proof with auto.
     split ; intros.
-    transitivity x0... transitivity x... symmetry...
+    - transitivity x0... transitivity x... symmetry...
 
-    transitivity y... transitivity y0... symmetry...
+    - transitivity y... transitivity y0... symmetry...
   Qed.
 
   Lemma symmetric_equiv_flip `(Symmetric A R) : relation_equivalence R (flip R).
@@ -403,15 +404,15 @@ Section GenericInstances.
     unfold respectful, relation_equivalence, predicate_equivalence in * ; simpl in *.
     split ; intros.
     
-    rewrite <- H0.
-    apply H1.
-    rewrite H.
-    assumption.
-    
-    rewrite H0.
-    apply H1.
-    rewrite <- H.
-    assumption.
+    - rewrite <- H0.
+      apply H1.
+      rewrite H.
+      assumption.
+
+    - rewrite H0.
+      apply H1.
+      rewrite <- H.
+      assumption.
   Qed.
 
   (** [R] is Reflexive, hence we can build the needed proof. *)
@@ -514,10 +515,10 @@ Proof.
   simpl_relation.
   reduce in H.
   split ; red ; intros.
-  setoid_rewrite <- H.
-  apply H0.
-  setoid_rewrite H.
-  apply H0.
+  - setoid_rewrite <- H.
+    apply H0.
+  - setoid_rewrite H.
+    apply H0.
 Qed.
 
 Ltac proper_reflexive :=
@@ -574,8 +575,8 @@ Proof.
   unfold relation_equivalence in *. 
   unfold predicate_equivalence in *. simpl in *.
   unfold respectful. unfold flip in *. firstorder.
-  apply NB. apply H. apply NA. apply H0.
-  apply NB. apply H. apply NA. apply H0.
+  - apply NB. apply H. apply NA. apply H0.
+  - apply NB. apply H. apply NA. apply H0.
 Qed.
 
 Ltac normalizes :=
@@ -642,9 +643,9 @@ intros.
 apply proper_sym_impl_iff_2; auto with *.
 intros x x' Hx y y' Hy Hr.
 transitivity x.
-generalize (partial_order_equivalence x x'); compute; intuition.
-transitivity y; auto.
-generalize (partial_order_equivalence y y'); compute; intuition.
+- generalize (partial_order_equivalence x x'); compute; intuition.
+- transitivity y; auto.
+  generalize (partial_order_equivalence y y'); compute; intuition.
 Qed.
 
 (** From a [PartialOrder] to the corresponding [StrictOrder]:
@@ -655,13 +656,13 @@ Lemma PartialOrder_StrictOrder `(PartialOrder A eqA R) :
   StrictOrder (relation_conjunction R (complement eqA)).
 Proof.
 split; compute.
-intros x (_,Hx). apply Hx, Equivalence_Reflexive.
-intros x y z (Hxy,Hxy') (Hyz,Hyz'). split.
-apply PreOrder_Transitive with y; assumption.
-intro Hxz.
-apply Hxy'.
-apply partial_order_antisym; auto.
-rewrite Hxz; auto.
+- intros x (_,Hx). apply Hx, Equivalence_Reflexive.
+- intros x y z (Hxy,Hxy') (Hyz,Hyz'). split.
+  + apply PreOrder_Transitive with y; assumption.
+  + intro Hxz.
+    apply Hxy'.
+    apply partial_order_antisym; auto.
+    rewrite Hxz; auto.
 Qed.
 
 
@@ -674,12 +675,12 @@ Lemma StrictOrder_PreOrder
  PreOrder (relation_disjunction R eqA).
 Proof.
 split.
-intros x. right. reflexivity.
-intros x y z [Hxy|Hxy] [Hyz|Hyz].
-left. transitivity y; auto.
-left. rewrite <- Hyz; auto.
-left. rewrite Hxy; auto.
-right. transitivity y; auto.
+- intros x. right. reflexivity.
+- intros x y z [Hxy|Hxy] [Hyz|Hyz].
+  + left. transitivity y; auto.
+  + left. rewrite <- Hyz; auto.
+  + left. rewrite Hxy; auto.
+  + right. transitivity y; auto.
 Qed.
 
 Hint Extern 4 (PreOrder (relation_disjunction _ _)) => 
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v
index 8881fda577..efb85aa341 100644
--- a/theories/Classes/Morphisms_Prop.v
+++ b/theories/Classes/Morphisms_Prop.v
@@ -85,10 +85,12 @@ Qed.
 Instance Acc_rel_morphism {A:Type} :
  Proper (relation_equivalence ==> Logic.eq ==> iff) (@Acc A).
 Proof.
- apply proper_sym_impl_iff_2. red; now symmetry. red; now symmetry.
- intros R R' EQ a a' Ha WF. subst a'.
- induction WF as [x _ WF']. constructor.
- intros y Ryx. now apply WF', EQ.
+  apply proper_sym_impl_iff_2.
+  - red; now symmetry.
+  - red; now symmetry.
+  - intros R R' EQ a a' Ha WF. subst a'.
+    induction WF as [x _ WF']. constructor.
+    intros y Ryx. now apply WF', EQ.
 Qed.
 
 (** Equivalent relations are simultaneously well-founded or not *)
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 6e2ff49536..440b317573 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -407,9 +407,10 @@ Program Instance predicate_equivalence_equivalence :
   Qed.
   Next Obligation.
     fold pointwise_lifting.
-    induction l. firstorder.
-    intros. simpl in *. pose (IHl (x x0) (y x0) (z x0)).
-    firstorder.
+    induction l.
+    - firstorder.
+    - intros. simpl in *. pose (IHl (x x0) (y x0) (z x0)).
+      firstorder.
   Qed.
 
 Program Instance predicate_implication_preorder :
@@ -418,9 +419,10 @@ Program Instance predicate_implication_preorder :
     induction l ; firstorder.
   Qed.
   Next Obligation.
-    induction l. firstorder.
-    unfold predicate_implication in *. simpl in *.
-    intro. pose (IHl (x x0) (y x0) (z x0)). firstorder.
+    induction l.
+    - firstorder.
+    - unfold predicate_implication in *. simpl in *.
+      intro. pose (IHl (x x0) (y x0) (z x0)). firstorder.
   Qed.
 
 (** We define the various operations which define the algebra on binary relations,