1 files changed, 241 insertions, 264 deletions

diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index 56ae921e..11d9a071 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -86,73 +86,50 @@ Module Z_as_Int <: Int.
   Definition int := Z.
   Definition zero := 0.
   Definition one := 1.
-  Definition plus := Zplus.
-  Definition opp := Zopp.
-  Definition minus := Zminus.
-  Definition mult := Zmult.
+  Definition plus := Z.add.
+  Definition opp := Z.opp.
+  Definition minus := Z.sub.
+  Definition mult := Z.mul.
 
   Lemma ring : @ring_theory int zero one plus mult minus opp (@eq int).
   Proof.
   constructor.
-  exact Zplus_0_l.
-  exact Zplus_comm.
-  exact Zplus_assoc.
-  exact Zmult_1_l.
-  exact Zmult_comm.
-  exact Zmult_assoc.
-  exact Zmult_plus_distr_l.
-  unfold minus, Zminus; auto.
-  exact Zplus_opp_r.
+  exact Z.add_0_l.
+  exact Z.add_comm.
+  exact Z.add_assoc.
+  exact Z.mul_1_l.
+  exact Z.mul_comm.
+  exact Z.mul_assoc.
+  exact Z.mul_add_distr_r.
+  unfold minus, Z.sub; auto.
+  exact Z.add_opp_diag_r.
   Qed.
 
-  Definition le := Zle.
-  Definition lt := Zlt.
-  Definition ge := Zge.
-  Definition gt := Zgt.
-  Lemma le_lt_iff : forall i j, (i<=j) <-> ~(j<i).
-  Proof.
-   split; intros.
-   apply Zle_not_lt; auto.
-   rewrite <- Zge_iff_le.
-   apply Znot_lt_ge; auto.
-  Qed.
-  Definition ge_le_iff := Zge_iff_le.
-  Definition gt_lt_iff := Zgt_iff_lt.
+  Definition le := Z.le.
+  Definition lt := Z.lt.
+  Definition ge := Z.ge.
+  Definition gt := Z.gt.
+  Definition le_lt_iff := Z.le_ngt.
+  Definition ge_le_iff := Z.ge_le_iff.
+  Definition gt_lt_iff := Z.gt_lt_iff.
 
-  Definition lt_trans := Zlt_trans.
-  Definition lt_not_eq := Zlt_not_eq.
+  Definition lt_trans := Z.lt_trans.
+  Definition lt_not_eq := Z.lt_neq.
 
-  Definition lt_0_1 := Zlt_0_1.
-  Definition plus_le_compat := Zplus_le_compat.
+  Definition lt_0_1 := Z.lt_0_1.
+  Definition plus_le_compat := Z.add_le_mono.
   Definition mult_lt_compat_l := Zmult_lt_compat_l.
-  Lemma opp_le_compat : forall i j, i<=j -> (-j)<=(-i).
-  Proof.
-  unfold Zle; intros; rewrite <- Zcompare_opp; auto.
-  Qed.
+  Lemma opp_le_compat i j : i<=j -> (-j)<=(-i).
+  Proof. apply -> Z.opp_le_mono. Qed.
 
-  Definition compare := Zcompare.
-  Definition compare_Eq := Zcompare_Eq_iff_eq.
-  Lemma compare_Lt : forall i j, compare i j = Lt <-> i<j.
-  Proof. intros; unfold compare, Zlt; intuition. Qed.
-  Lemma compare_Gt : forall i j, compare i j = Gt <-> i>j.
-  Proof. intros; unfold compare, Zgt; intuition. Qed.
+  Definition compare := Z.compare.
+  Definition compare_Eq := Z.compare_eq_iff.
+  Lemma compare_Lt i j : compare i j = Lt <-> i<j.
+  Proof. reflexivity. Qed.
+  Lemma compare_Gt i j : compare i j = Gt <-> i>j.
+  Proof. reflexivity. Qed.
 
-  Lemma le_lt_int : forall x y, x<y <-> x<=y+-(1).
-  Proof.
-   intros; split; intros.
-   generalize (Zlt_left _ _ H); simpl; intros.
-   apply Zle_left_rev; auto.
-   apply Zlt_0_minus_lt.
-   generalize (Zplus_le_lt_compat x (y+-1) (-x) (-x+1) H).
-   rewrite Zplus_opp_r.
-   rewrite <-Zplus_assoc.
-   rewrite (Zplus_permute (-1)).
-   simpl in *.
-   rewrite Zplus_0_r.
-   intro H'; apply H'.
-   replace (-x+1) with (Zsucc (-x)); auto.
-   apply Zlt_succ.
-  Qed.
+  Definition le_lt_int := Z.lt_le_pred.
 
 End Z_as_Int.
 
@@ -363,7 +340,7 @@ Module IntProperties (I:Int).
 
  Lemma sum1 : forall a b c d : int, 0 = a -> 0 = b -> 0 = a * c + b * d.
  Proof.
- intros; elim H; elim H0; simpl in |- *; auto.
+ intros; elim H; elim H0; simpl; auto.
  now rewrite mult_0_l, mult_0_l, plus_0_l.
  Qed.
 
@@ -1076,34 +1053,34 @@ Proof.
  | intros; elim beq_nat_true with (1 := H); trivial ].
 Qed.
 
-Ltac trivial_case := unfold not in |- *; intros; discriminate.
+Ltac trivial_case := unfold not; intros; discriminate.
 
 Theorem eq_term_false :
  forall t1 t2 : term, eq_term t1 t2 = false -> t1 <> t2.
 Proof.
  simple induction t1;
- [ intros z t2; case t2; try trivial_case; simpl in |- *; unfold not in |- *;
+ [ intros z t2; case t2; try trivial_case; simpl; unfold not;
     intros; elim beq_false with (1 := H); simplify_eq H0;
     auto
- | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl in |- *;
-    intros t21 t22 H3; unfold not in |- *; intro H4;
+ | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl;
+    intros t21 t22 H3; unfold not; intro H4;
     elim andb_false_elim with (1 := H3); intros H5;
     [ elim H1 with (1 := H5); simplify_eq H4; auto
     | elim H2 with (1 := H5); simplify_eq H4; auto ]
- | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl in |- *;
-    intros t21 t22 H3; unfold not in |- *; intro H4;
+ | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl;
+    intros t21 t22 H3; unfold not; intro H4;
     elim andb_false_elim with (1 := H3); intros H5;
     [ elim H1 with (1 := H5); simplify_eq H4; auto
     | elim H2 with (1 := H5); simplify_eq H4; auto ]
- | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl in |- *;
-    intros t21 t22 H3; unfold not in |- *; intro H4;
+ | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl;
+    intros t21 t22 H3; unfold not; intro H4;
     elim andb_false_elim with (1 := H3); intros H5;
     [ elim H1 with (1 := H5); simplify_eq H4; auto
     | elim H2 with (1 := H5); simplify_eq H4; auto ]
- | intros t11 H1 t2; case t2; try trivial_case; simpl in |- *; intros t21 H3;
-    unfold not in |- *; intro H4; elim H1 with (1 := H3);
+ | intros t11 H1 t2; case t2; try trivial_case; simpl; intros t21 H3;
+    unfold not; intro H4; elim H1 with (1 := H3);
     simplify_eq H4; auto
- | intros n t2; case t2; try trivial_case; simpl in |- *; unfold not in |- *;
+ | intros n t2; case t2; try trivial_case; simpl; unfold not;
     intros; elim beq_nat_false with (1 := H); simplify_eq H0;
     auto ].
 Qed.
@@ -1123,17 +1100,17 @@ Qed.
    avait utilisé le test précédent et fait une elimination dessus. *)
 
 Ltac elim_eq_term t1 t2 :=
-  pattern (eq_term t1 t2) in |- *; apply bool_eq_ind; intro Aux;
+  pattern (eq_term t1 t2); apply bool_eq_ind; intro Aux;
    [ generalize (eq_term_true t1 t2 Aux); clear Aux
    | generalize (eq_term_false t1 t2 Aux); clear Aux ].
 
 Ltac elim_beq t1 t2 :=
-  pattern (beq t1 t2) in |- *; apply bool_eq_ind; intro Aux;
+  pattern (beq t1 t2); apply bool_eq_ind; intro Aux;
    [ generalize (beq_true t1 t2 Aux); clear Aux
    | generalize (beq_false t1 t2 Aux); clear Aux ].
 
 Ltac elim_bgt t1 t2 :=
-  pattern (bgt t1 t2) in |- *; apply bool_eq_ind; intro Aux;
+  pattern (bgt t1 t2); apply bool_eq_ind; intro Aux;
   [ generalize (bgt_true t1 t2 Aux); clear Aux
   | generalize (bgt_false t1 t2 Aux); clear Aux ].
 
@@ -1209,15 +1186,15 @@ Theorem goal_to_hyps :
  (interp_hyps envp env l -> False) -> interp_goal envp env l.
 Proof.
  simple induction l;
- [ simpl in |- *; auto
- | simpl in |- *; intros a l1 H1 H2 H3; apply H1; intro H4; apply H2; auto ].
+ [ simpl; auto
+ | simpl; intros a l1 H1 H2 H3; apply H1; intro H4; apply H2; auto ].
 Qed.
 
 Theorem hyps_to_goal :
  forall (envp : list Prop) (env : list int) (l : hyps),
  interp_goal envp env l -> interp_hyps envp env l -> False.
 Proof.
- simple induction l; simpl in |- *; [ auto | intros; apply H; elim H1; auto ].
+ simple induction l; simpl; [ auto | intros; apply H; elim H1; auto ].
 Qed.
 
 (* \subsection{Manipulations sur les hypothèses} *)
@@ -1257,7 +1234,7 @@ Theorem valid_goal :
   forall (ep : list Prop) (env : list int) (l : hyps) (a : hyps -> hyps),
   valid_hyps a -> interp_goal ep env (a l) -> interp_goal ep env l.
 Proof.
- intros; simpl in |- *; apply goal_to_hyps; intro H1;
+ intros; simpl; apply goal_to_hyps; intro H1;
  apply (hyps_to_goal ep env (a l) H0); apply H; assumption.
 Qed.
 
@@ -1282,7 +1259,7 @@ Theorem list_goal_to_hyps :
  forall (envp : list Prop) (env : list int) (l : lhyps),
  (interp_list_hyps envp env l -> False) -> interp_list_goal envp env l.
 Proof.
- simple induction l; simpl in |- *;
+ simple induction l; simpl;
  [ auto
  | intros h1 l1 H H1; split;
     [ apply goal_to_hyps; intro H2; apply H1; auto
@@ -1293,7 +1270,7 @@ Theorem list_hyps_to_goal :
  forall (envp : list Prop) (env : list int) (l : lhyps),
  interp_list_goal envp env l -> interp_list_hyps envp env l -> False.
 Proof.
- simple induction l; simpl in |- *;
+ simple induction l; simpl;
  [ auto
  | intros h1 l1 H (H1, H2) H3; elim H3; intro H4;
     [ apply hyps_to_goal with (1 := H1); assumption | auto ] ].
@@ -1310,7 +1287,7 @@ Definition valid_list_goal (f : hyps -> lhyps) :=
 Theorem goal_valid :
  forall f : hyps -> lhyps, valid_list_hyps f -> valid_list_goal f.
 Proof.
- unfold valid_list_goal in |- *; intros f H ep e lp H1; apply goal_to_hyps;
+ unfold valid_list_goal; intros f H ep e lp H1; apply goal_to_hyps;
  intro H2; apply list_hyps_to_goal with (1 := H1);
  apply (H ep e lp); assumption.
 Qed.
@@ -1321,8 +1298,8 @@ Theorem append_valid :
  interp_list_hyps ep e (l1 ++ l2).
 Proof.
  intros ep e; simple induction l1;
- [ simpl in |- *; intros l2 [H| H]; [ contradiction | trivial ]
- | simpl in |- *; intros h1 t1 HR l2 [[H| H]| H];
+ [ simpl; intros l2 [H| H]; [ contradiction | trivial ]
+ | simpl; intros h1 t1 HR l2 [[H| H]| H];
     [ auto
     | right; apply (HR l2); left; trivial
     | right; apply (HR l2); right; trivial ] ].
@@ -1338,11 +1315,11 @@ Theorem nth_valid :
  forall (ep : list Prop) (e : list int) (i : nat) (l : hyps),
  interp_hyps ep e l -> interp_proposition ep e (nth_hyps i l).
 Proof.
- unfold nth_hyps in |- *; simple induction i;
- [ simple induction l; simpl in |- *; [ auto | intros; elim H0; auto ]
+ unfold nth_hyps; simple induction i;
+ [ simple induction l; simpl; [ auto | intros; elim H0; auto ]
  | intros n H; simple induction l;
-    [ simpl in |- *; trivial
-    | intros; simpl in |- *; apply H; elim H1; auto ] ].
+    [ simpl; trivial
+    | intros; simpl; apply H; elim H1; auto ] ].
 Qed.
 
 (* Appliquer une opération (valide) sur deux hypothèses extraites de
@@ -1355,7 +1332,7 @@ Theorem apply_oper_2_valid :
  forall (i j : nat) (f : proposition -> proposition -> proposition),
  valid2 f -> valid_hyps (apply_oper_2 i j f).
 Proof.
- intros i j f Hf; unfold apply_oper_2, valid_hyps in |- *; simpl in |- *;
+ intros i j f Hf; unfold apply_oper_2, valid_hyps; simpl;
  intros lp Hlp; split; [ apply Hf; apply nth_valid; assumption | assumption ].
 Qed.
 
@@ -1376,14 +1353,14 @@ Theorem apply_oper_1_valid :
  forall (i : nat) (f : proposition -> proposition),
  valid1 f -> valid_hyps (apply_oper_1 i f).
 Proof.
- unfold valid_hyps in |- *; intros i f Hf ep e; elim i;
+ unfold valid_hyps; intros i f Hf ep e; elim i;
  [ intro lp; case lp;
-    [ simpl in |- *; trivial
-    | simpl in |- *; intros p l' (H1, H2); split;
+    [ simpl; trivial
+    | simpl; intros p l' (H1, H2); split;
        [ apply Hf with (1 := H1) | assumption ] ]
  | intros n Hrec lp; case lp;
-    [ simpl in |- *; auto
-    | simpl in |- *; intros p l' (H1, H2); split;
+    [ simpl; auto
+    | simpl; intros p l' (H1, H2); split;
        [ assumption | apply Hrec; assumption ] ] ].
 Qed.
 
@@ -1421,14 +1398,14 @@ Definition apply_both (f g : term -> term) (t : term) :=
 Theorem apply_left_stable :
  forall f : term -> term, term_stable f -> term_stable (apply_left f).
 Proof.
- unfold term_stable in |- *; intros f H e t; case t; auto; simpl in |- *;
+ unfold term_stable; intros f H e t; case t; auto; simpl;
  intros; elim H; trivial.
 Qed.
 
 Theorem apply_right_stable :
  forall f : term -> term, term_stable f -> term_stable (apply_right f).
 Proof.
- unfold term_stable in |- *; intros f H e t; case t; auto; simpl in |- *;
+ unfold term_stable; intros f H e t; case t; auto; simpl;
  intros t0 t1; elim H; trivial.
 Qed.
 
@@ -1436,7 +1413,7 @@ Theorem apply_both_stable :
  forall f g : term -> term,
  term_stable f -> term_stable g -> term_stable (apply_both f g).
 Proof.
- unfold term_stable in |- *; intros f g H1 H2 e t; case t; auto; simpl in |- *;
+ unfold term_stable; intros f g H1 H2 e t; case t; auto; simpl;
  intros t0 t1; elim H1; elim H2; trivial.
 Qed.
 
@@ -1444,7 +1421,7 @@ Theorem compose_term_stable :
  forall f g : term -> term,
  term_stable f -> term_stable g -> term_stable (fun t : term => f (g t)).
 Proof.
- unfold term_stable in |- *; intros f g Hf Hg e t; elim Hf; apply Hg.
+ unfold term_stable; intros f g Hf Hg e t; elim Hf; apply Hg.
 Qed.
 
 (* \subsection{Les règles de réécriture} *)
@@ -1522,14 +1499,14 @@ Ltac loop t :=
   | (if beq ?X1 ?X2 then _ else _) =>
       let H := fresh "H" in
       elim_beq X1 X2; intro H; try (rewrite H in *; clear H);
-       simpl in |- *; auto; Simplify
+       simpl; auto; Simplify
   | (if bgt ?X1 ?X2 then _ else _) =>
       let H := fresh "H" in
-      elim_bgt X1 X2; intro H; simpl in |- *; auto; Simplify
+      elim_bgt X1 X2; intro H; simpl; auto; Simplify
   | (if eq_term ?X1 ?X2 then _ else _) =>
       let H := fresh "H" in
       elim_eq_term X1 X2; intro H; try (rewrite H in *; clear H);
-       simpl in |- *; auto; Simplify
+       simpl; auto; Simplify
   | (if _ && _ then _ else _) => rewrite andb_if; Simplify
   | (if negb _ then _ else _) => rewrite negb_if; Simplify
   | _ => fail
@@ -1543,7 +1520,7 @@ with Simplify := match goal with
 Ltac prove_stable x th :=
   match constr:x with
   | ?X1 =>
-      unfold term_stable, X1 in |- *; intros; Simplify; simpl in |- *;
+      unfold term_stable, X1; intros; Simplify; simpl;
        apply th
   end.
 
@@ -1663,7 +1640,7 @@ Definition T_OMEGA13 (t : term) :=
 
 Theorem T_OMEGA13_stable : term_stable T_OMEGA13.
 Proof.
- unfold term_stable, T_OMEGA13 in |- *; intros; Simplify; simpl in |- *;
+ unfold term_stable, T_OMEGA13; intros; Simplify; simpl;
  apply OMEGA13.
 Qed.
 
@@ -1910,16 +1887,16 @@ Fixpoint reduce (t : term) : term :=
 
 Theorem reduce_stable : term_stable reduce.
 Proof.
- unfold term_stable in |- *; intros e t; elim t; auto;
+ unfold term_stable; intros e t; elim t; auto;
  try
-  (intros t0 H0 t1 H1; simpl in |- *; rewrite H0; rewrite H1;
+  (intros t0 H0 t1 H1; simpl; rewrite H0; rewrite H1;
     (case (reduce t0);
       [ intro z0; case (reduce t1); intros; auto
       | intros; auto
       | intros; auto
       | intros; auto
       | intros; auto
-      | intros; auto ])); intros t0 H0; simpl in |- *;
+      | intros; auto ])); intros t0 H0; simpl;
  rewrite H0; case (reduce t0); intros; auto.
 Qed.
 
@@ -1944,12 +1921,12 @@ Fixpoint fusion (trace : list t_fusion) (t : term) {struct trace} : term :=
 
 Theorem fusion_stable : forall t : list t_fusion, term_stable (fusion t).
 Proof.
- simple induction t; simpl in |- *;
+ simple induction t; simpl;
  [ exact reduce_stable
  | intros stp l H; case stp;
     [ apply compose_term_stable;
        [ apply apply_right_stable; assumption | exact T_OMEGA10_stable ]
-    | unfold term_stable in |- *; intros e t1; rewrite T_OMEGA10_stable;
+    | unfold term_stable; intros e t1; rewrite T_OMEGA10_stable;
        rewrite Tred_factor5_stable; apply H
     | apply compose_term_stable;
        [ apply apply_right_stable; assumption | exact T_OMEGA11_stable ]
@@ -1982,7 +1959,7 @@ Fixpoint fusion_cancel (trace : nat) (t : term) {struct trace} : term :=
 
 Theorem fusion_cancel_stable : forall t : nat, term_stable (fusion_cancel t).
 Proof.
- unfold term_stable, fusion_cancel in |- *; intros trace e; elim trace;
+ unfold term_stable, fusion_cancel; intros trace e; elim trace;
  [ exact (reduce_stable e)
  | intros n H t; elim H; exact (T_OMEGA13_stable e t) ].
 Qed.
@@ -1999,7 +1976,7 @@ Fixpoint scalar_norm_add (trace : nat) (t : term) {struct trace} : term :=
 Theorem scalar_norm_add_stable :
  forall t : nat, term_stable (scalar_norm_add t).
 Proof.
- unfold term_stable, scalar_norm_add in |- *; intros trace; elim trace;
+ unfold term_stable, scalar_norm_add; intros trace; elim trace;
  [ exact reduce_stable
  | intros n H e t; elim apply_right_stable;
     [ exact (T_OMEGA11_stable e t) | exact H ] ].
@@ -2014,7 +1991,7 @@ Fixpoint scalar_norm (trace : nat) (t : term) {struct trace} : term :=
 
 Theorem scalar_norm_stable : forall t : nat, term_stable (scalar_norm t).
 Proof.
- unfold term_stable, scalar_norm in |- *; intros trace; elim trace;
+ unfold term_stable, scalar_norm; intros trace; elim trace;
  [ exact reduce_stable
  | intros n H e t; elim apply_right_stable;
     [ exact (T_OMEGA16_stable e t) | exact H ] ].
@@ -2029,7 +2006,7 @@ Fixpoint add_norm (trace : nat) (t : term) {struct trace} : term :=
 
 Theorem add_norm_stable : forall t : nat, term_stable (add_norm t).
 Proof.
- unfold term_stable, add_norm in |- *; intros trace; elim trace;
+ unfold term_stable, add_norm; intros trace; elim trace;
  [ exact reduce_stable
  | intros n H e t; elim apply_right_stable;
     [ exact (Tplus_assoc_r_stable e t) | exact H ] ].
@@ -2071,12 +2048,12 @@ Fixpoint t_rewrite (s : step) : term -> term :=
 
 Theorem t_rewrite_stable : forall s : step, term_stable (t_rewrite s).
 Proof.
- simple induction s; simpl in |- *;
+ simple induction s; simpl;
  [ intros; apply apply_both_stable; auto
  | intros; apply apply_left_stable; auto
  | intros; apply apply_right_stable; auto
- | unfold term_stable in |- *; intros; elim H0; apply H
- | unfold term_stable in |- *; auto
+ | unfold term_stable; intros; elim H0; apply H
+ | unfold term_stable; auto
  | exact Topp_plus_stable
  | exact Topp_opp_stable
  | exact Topp_mult_r_stable
@@ -2116,11 +2093,11 @@ Definition constant_not_nul (i : nat) (h : hyps) :=
 Theorem constant_not_nul_valid :
  forall i : nat, valid_hyps (constant_not_nul i).
 Proof.
- unfold valid_hyps, constant_not_nul in |- *; intros;
- generalize (nth_valid ep e i lp); Simplify; simpl in |- *.
+ unfold valid_hyps, constant_not_nul; intros;
+ generalize (nth_valid ep e i lp); Simplify; simpl.
 
- elim_beq i1 i0; auto; simpl in |- *; intros H1 H2;
- elim H1; symmetry  in |- *; auto.
+ elim_beq i1 i0; auto; simpl; intros H1 H2;
+ elim H1; symmetry ; auto.
 Qed.
 
 (* \paragraph{[O_CONSTANT_NEG]} *)
@@ -2134,8 +2111,8 @@ Definition constant_neg (i : nat) (h : hyps) :=
 
 Theorem constant_neg_valid : forall i : nat, valid_hyps (constant_neg i).
 Proof.
- unfold valid_hyps, constant_neg in |- *; intros;
- generalize (nth_valid ep e i lp); Simplify; simpl in |- *.
+ unfold valid_hyps, constant_neg; intros;
+ generalize (nth_valid ep e i lp); Simplify; simpl.
  rewrite gt_lt_iff in H0; rewrite le_lt_iff; intuition.
 Qed.
 
@@ -2157,7 +2134,7 @@ Theorem not_exact_divide_valid :
  forall (k1 k2 : int) (body : term) (t i : nat),
  valid_hyps (not_exact_divide k1 k2 body t i).
 Proof.
- unfold valid_hyps, not_exact_divide in |- *; intros;
+ unfold valid_hyps, not_exact_divide; intros;
  generalize (nth_valid ep e i lp); Simplify.
  rewrite (scalar_norm_add_stable t e), <-H1.
  do 2 rewrite <- scalar_norm_add_stable; simpl in *; intros.
@@ -2186,16 +2163,16 @@ Definition contradiction (t i j : nat) (l : hyps) :=
 Theorem contradiction_valid :
  forall t i j : nat, valid_hyps (contradiction t i j).
 Proof.
- unfold valid_hyps, contradiction in |- *; intros t i j ep e l H;
+ unfold valid_hyps, contradiction; intros t i j ep e l H;
  generalize (nth_valid _ _ i _ H); generalize (nth_valid _ _ j _ H);
  case (nth_hyps i l); auto; intros t1 t2; case t1;
  auto; case (nth_hyps j l);
  auto; intros t3 t4; case t3; auto;
- simpl in |- *; intros z z' H1 H2;
- generalize (refl_equal (interp_term e (fusion_cancel t (t2 + t4)%term)));
- pattern (fusion_cancel t (t2 + t4)%term) at 2 3 in |- *;
- case (fusion_cancel t (t2 + t4)%term); simpl in |- *;
- auto; intro k; elim (fusion_cancel_stable t); simpl in |- *.
+ simpl; intros z z' H1 H2;
+ generalize (eq_refl (interp_term e (fusion_cancel t (t2 + t4)%term)));
+ pattern (fusion_cancel t (t2 + t4)%term) at 2 3;
+ case (fusion_cancel t (t2 + t4)%term); simpl;
+ auto; intro k; elim (fusion_cancel_stable t); simpl.
  Simplify; intro H3.
  generalize (OMEGA2 _ _ H2 H1); rewrite H3.
  rewrite gt_lt_iff in H0; rewrite le_lt_iff; intuition.
@@ -2250,23 +2227,23 @@ Definition negate_contradict_inv (t i1 i2 : nat) (h : hyps) :=
 Theorem negate_contradict_valid :
  forall i j : nat, valid_hyps (negate_contradict i j).
 Proof.
- unfold valid_hyps, negate_contradict in |- *; intros i j ep e l H;
+ unfold valid_hyps, negate_contradict; intros i j ep e l H;
  generalize (nth_valid _ _ i _ H); generalize (nth_valid _ _ j _ H);
  case (nth_hyps i l); auto; intros t1 t2; case t1;
  auto; intros z; auto; case (nth_hyps j l);
  auto; intros t3 t4; case t3; auto; intros z';
- auto; simpl in |- *; intros H1 H2; Simplify.
+ auto; simpl; intros H1 H2; Simplify.
 Qed.
 
 Theorem negate_contradict_inv_valid :
  forall t i j : nat, valid_hyps (negate_contradict_inv t i j).
 Proof.
- unfold valid_hyps, negate_contradict_inv in |- *; intros t i j ep e l H;
+ unfold valid_hyps, negate_contradict_inv; intros t i j ep e l H;
  generalize (nth_valid _ _ i _ H); generalize (nth_valid _ _ j _ H);
  case (nth_hyps i l); auto; intros t1 t2; case t1;
  auto; intros z; auto; case (nth_hyps j l);
  auto; intros t3 t4; case t3; auto; intros z';
- auto; simpl in |- *; intros H1 H2; Simplify;
+ auto; simpl; intros H1 H2; Simplify;
  [
  rewrite <- scalar_norm_stable in H2; simpl in *;
  elim (mult_integral (interp_term e t4) (-(1))); intuition;
@@ -2333,9 +2310,9 @@ Definition sum (k1 k2 : int) (trace : list t_fusion)
 Theorem sum_valid :
  forall (k1 k2 : int) (t : list t_fusion), valid2 (sum k1 k2 t).
 Proof.
- unfold valid2 in |- *; intros k1 k2 t ep e p1 p2; unfold sum in |- *;
- Simplify; simpl in |- *; auto; try elim (fusion_stable t);
- simpl in |- *; intros;
+ unfold valid2; intros k1 k2 t ep e p1 p2; unfold sum;
+ Simplify; simpl; auto; try elim (fusion_stable t);
+ simpl; intros;
  [ apply sum1; assumption
  | apply sum2; try assumption; apply sum4; assumption
  | rewrite plus_comm; apply sum2; try assumption; apply sum4; assumption
@@ -2367,10 +2344,10 @@ Definition exact_divide (k : int) (body : term) (t : nat)
 Theorem exact_divide_valid :
  forall (k : int) (t : term) (n : nat), valid1 (exact_divide k t n).
 Proof.
- unfold valid1, exact_divide in |- *; intros k1 k2 t ep e p1;
+ unfold valid1, exact_divide; intros k1 k2 t ep e p1;
  Simplify; simpl; auto; subst;
  rewrite <- scalar_norm_stable; simpl; intros;
- [ destruct (mult_integral _ _ (sym_eq H0)); intuition
+ [ destruct (mult_integral _ _ (eq_sym H0)); intuition
  | contradict H0; rewrite <- H0, mult_0_l; auto
  ].
 Qed.
@@ -2397,9 +2374,9 @@ Theorem divide_and_approx_valid :
  forall (k1 k2 : int) (body : term) (t : nat),
  valid1 (divide_and_approx k1 k2 body t).
 Proof.
- unfold valid1, divide_and_approx in |- *; intros k1 k2 body t ep e p1;
+ unfold valid1, divide_and_approx; intros k1 k2 body t ep e p1;
  Simplify; simpl; auto; subst;
- elim (scalar_norm_add_stable t e); simpl in |- *.
+ elim (scalar_norm_add_stable t e); simpl.
  intro H2; apply mult_le_approx with (3 := H2); assumption.
 Qed.
 
@@ -2421,9 +2398,9 @@ Definition merge_eq (t : nat) (prop1 prop2 : proposition) :=
 
 Theorem merge_eq_valid : forall n : nat, valid2 (merge_eq n).
 Proof.
- unfold valid2, merge_eq in |- *; intros n ep e p1 p2; Simplify; simpl in |- *;
- auto; elim (scalar_norm_stable n e); simpl in |- *;
- intros; symmetry  in |- *; apply OMEGA8 with (2 := H0);
+ unfold valid2, merge_eq; intros n ep e p1 p2; Simplify; simpl;
+ auto; elim (scalar_norm_stable n e); simpl;
+ intros; symmetry ; apply OMEGA8 with (2 := H0);
  [ assumption | elim opp_eq_mult_neg_1; trivial ].
 Qed.
 
@@ -2440,8 +2417,8 @@ Definition constant_nul (i : nat) (h : hyps) :=
 
 Theorem constant_nul_valid : forall i : nat, valid_hyps (constant_nul i).
 Proof.
- unfold valid_hyps, constant_nul in |- *; intros;
- generalize (nth_valid ep e i lp); Simplify; simpl in |- *;
+ unfold valid_hyps, constant_nul; intros;
+ generalize (nth_valid ep e i lp); Simplify; simpl;
  intro H1; absurd (0 = 0); intuition.
 Qed.
 
@@ -2462,8 +2439,8 @@ Definition state (m : int) (s : step) (prop1 prop2 : proposition) :=
 
 Theorem state_valid : forall (m : int) (s : step), valid2 (state m s).
 Proof.
- unfold valid2 in |- *; intros m s ep e p1 p2; unfold state in |- *; Simplify;
- simpl in |- *; auto; elim (t_rewrite_stable s e); simpl in |- *;
+ unfold valid2; intros m s ep e p1 p2; unfold state; Simplify;
+ simpl; auto; elim (t_rewrite_stable s e); simpl;
  intros H1 H2; elim H1.
  now rewrite H2, plus_opp_l, plus_0_l, mult_0_l.
 Qed.
@@ -2490,18 +2467,18 @@ Theorem split_ineq_valid :
  valid_list_hyps f1 ->
  valid_list_hyps f2 -> valid_list_hyps (split_ineq i t f1 f2).
 Proof.
- unfold valid_list_hyps, split_ineq in |- *; intros i t f1 f2 H1 H2 ep e lp H;
+ unfold valid_list_hyps, split_ineq; intros i t f1 f2 H1 H2 ep e lp H;
  generalize (nth_valid _ _ i _ H); case (nth_hyps i lp);
- simpl in |- *; auto; intros t1 t2; case t1; simpl in |- *;
- auto; intros z; simpl in |- *; auto; intro H3.
+ simpl; auto; intros t1 t2; case t1; simpl;
+ auto; intros z; simpl; auto; intro H3.
  Simplify.
  apply append_valid; elim (OMEGA19 (interp_term e t2));
- [ intro H4; left; apply H1; simpl in |- *; elim (add_norm_stable t);
-    simpl in |- *; auto
- | intro H4; right; apply H2; simpl in |- *; elim (scalar_norm_add_stable t);
-    simpl in |- *; auto
- | generalize H3; unfold not in |- *; intros E1 E2; apply E1;
-    symmetry  in |- *; trivial ].
+ [ intro H4; left; apply H1; simpl; elim (add_norm_stable t);
+    simpl; auto
+ | intro H4; right; apply H2; simpl; elim (scalar_norm_add_stable t);
+    simpl; auto
+ | generalize H3; unfold not; intros E1 E2; apply E1;
+    symmetry ; trivial ].
 Qed.
 
 
@@ -2534,47 +2511,47 @@ Fixpoint execute_omega (t : t_omega) (l : hyps) {struct t} : lhyps :=
 
 Theorem omega_valid : forall t : t_omega, valid_list_hyps (execute_omega t).
 Proof.
- simple induction t; simpl in |- *;
- [ unfold valid_list_hyps in |- *; simpl in |- *; intros; left;
+ simple induction t; simpl;
+ [ unfold valid_list_hyps; simpl; intros; left;
     apply (constant_not_nul_valid n ep e lp H)
- | unfold valid_list_hyps in |- *; simpl in |- *; intros; left;
+ | unfold valid_list_hyps; simpl; intros; left;
     apply (constant_neg_valid n ep e lp H)
- | unfold valid_list_hyps, valid_hyps in |- *;
+ | unfold valid_list_hyps, valid_hyps;
     intros k1 k2 body n t' Ht' m ep e lp H; apply Ht';
     apply
      (apply_oper_1_valid m (divide_and_approx k1 k2 body n)
         (divide_and_approx_valid k1 k2 body n) ep e lp H)
- | unfold valid_list_hyps in |- *; simpl in |- *; intros; left;
+ | unfold valid_list_hyps; simpl; intros; left;
     apply (not_exact_divide_valid i i0 t0 n n0 ep e lp H)
- | unfold valid_list_hyps, valid_hyps in |- *;
+ | unfold valid_list_hyps, valid_hyps;
     intros k body n t' Ht' m ep e lp H; apply Ht';
     apply
      (apply_oper_1_valid m (exact_divide k body n)
         (exact_divide_valid k body n) ep e lp H)
- | unfold valid_list_hyps, valid_hyps in |- *;
+ | unfold valid_list_hyps, valid_hyps;
     intros k1 i1 k2 i2 trace t' Ht' ep e lp H; apply Ht';
     apply
      (apply_oper_2_valid i1 i2 (sum k1 k2 trace) (sum_valid k1 k2 trace) ep e
         lp H)
- | unfold valid_list_hyps in |- *; simpl in |- *; intros; left;
+ | unfold valid_list_hyps; simpl; intros; left;
     apply (contradiction_valid n n0 n1 ep e lp H)
- | unfold valid_list_hyps, valid_hyps in |- *;
+ | unfold valid_list_hyps, valid_hyps;
     intros trace i1 i2 t' Ht' ep e lp H; apply Ht';
     apply
      (apply_oper_2_valid i1 i2 (merge_eq trace) (merge_eq_valid trace) ep e
         lp H)
- | intros t' i k1 H1 k2 H2; unfold valid_list_hyps in |- *; simpl in |- *;
+ | intros t' i k1 H1 k2 H2; unfold valid_list_hyps; simpl;
     intros ep e lp H;
     apply
      (split_ineq_valid i t' (execute_omega k1) (execute_omega k2) H1 H2 ep e
         lp H)
- | unfold valid_list_hyps in |- *; simpl in |- *; intros i ep e lp H; left;
+ | unfold valid_list_hyps; simpl; intros i ep e lp H; left;
     apply (constant_nul_valid i ep e lp H)
- | unfold valid_list_hyps in |- *; simpl in |- *; intros i j ep e lp H; left;
+ | unfold valid_list_hyps; simpl; intros i j ep e lp H; left;
     apply (negate_contradict_valid i j ep e lp H)
- | unfold valid_list_hyps in |- *; simpl in |- *; intros n i j ep e lp H;
+ | unfold valid_list_hyps; simpl; intros n i j ep e lp H;
     left; apply (negate_contradict_inv_valid n i j ep e lp H)
- | unfold valid_list_hyps, valid_hyps in |- *;
+ | unfold valid_list_hyps, valid_hyps;
     intros m s i1 i2 t' Ht' ep e lp H; apply Ht';
     apply (apply_oper_2_valid i1 i2 (state m s) (state_valid m s) ep e lp H) ].
 Qed.
@@ -2596,9 +2573,9 @@ Definition move_right (s : step) (p : proposition) :=
 
 Theorem move_right_valid : forall s : step, valid1 (move_right s).
 Proof.
- unfold valid1, move_right in |- *; intros s ep e p; Simplify; simpl in |- *;
- elim (t_rewrite_stable s e); simpl in |- *;
- [ symmetry  in |- *; apply egal_left; assumption
+ unfold valid1, move_right; intros s ep e p; Simplify; simpl;
+ elim (t_rewrite_stable s e); simpl;
+ [ symmetry ; apply egal_left; assumption
  | intro; apply le_left; assumption
  | intro; apply le_left; rewrite <- ge_le_iff; assumption
  | intro; apply lt_left; rewrite <- gt_lt_iff; assumption
@@ -2611,7 +2588,7 @@ Definition do_normalize (i : nat) (s : step) := apply_oper_1 i (move_right s).
 Theorem do_normalize_valid :
  forall (i : nat) (s : step), valid_hyps (do_normalize i s).
 Proof.
- intros; unfold do_normalize in |- *; apply apply_oper_1_valid;
+ intros; unfold do_normalize; apply apply_oper_1_valid;
  apply move_right_valid.
 Qed.
 
@@ -2625,7 +2602,7 @@ Fixpoint do_normalize_list (l : list step) (i : nat)
 Theorem do_normalize_list_valid :
  forall (l : list step) (i : nat), valid_hyps (do_normalize_list l i).
 Proof.
- simple induction l; simpl in |- *; unfold valid_hyps in |- *;
+ simple induction l; simpl; unfold valid_hyps;
  [ auto
  | intros a l' Hl' i ep e lp H; unfold valid_hyps in Hl'; apply Hl';
     apply (do_normalize_valid i a ep e lp); assumption ].
@@ -2654,8 +2631,8 @@ Theorem append_goal :
  interp_list_goal ep e (l1 ++ l2).
 Proof.
  intros ep e; simple induction l1;
- [ simpl in |- *; intros l2 (H1, H2); assumption
- | simpl in |- *; intros h1 t1 HR l2 ((H1, H2), H3); split; auto ].
+ [ simpl; intros l2 (H1, H2); assumption
+ | simpl; intros h1 t1 HR l2 ((H1, H2), H3); split; auto ].
 Qed.
 
 (* A simple decidability checker : if the proposition belongs to the
@@ -2684,11 +2661,11 @@ Theorem decidable_correct :
  forall (ep : list Prop) (e : list int) (p : proposition),
  decidability p = true -> decidable (interp_proposition ep e p).
 Proof.
- simple induction p; simpl in |- *; intros;
+ simple induction p; simpl; intros;
  [ apply dec_eq
  | apply dec_le
  | left; auto
- | right; unfold not in |- *; auto
+ | right; unfold not; auto
  | apply dec_not; auto
  | apply dec_ge
  | apply dec_gt
@@ -2724,7 +2701,7 @@ Theorem interp_full_false :
  forall (ep : list Prop) (e : list int) (l : hyps) (c : proposition),
  (interp_hyps ep e l -> interp_proposition ep e c) -> interp_full ep e (l, c).
 Proof.
- simple induction l; unfold interp_full in |- *; simpl in |- *;
+ simple induction l; unfold interp_full; simpl;
  [ auto | intros a l1 H1 c H2 H3; apply H1; auto ].
 Qed.
 
@@ -2744,12 +2721,12 @@ Theorem to_contradict_valid :
  forall (ep : list Prop) (e : list int) (lc : hyps * proposition),
  interp_goal ep e (to_contradict lc) -> interp_full ep e lc.
 Proof.
- intros ep e lc; case lc; intros l c; simpl in |- *;
- pattern (decidability c) in |- *; apply bool_eq_ind;
- [ simpl in |- *; intros H H1; apply interp_full_false; intros H2;
+ intros ep e lc; case lc; intros l c; simpl;
+ pattern (decidability c); apply bool_eq_ind;
+ [ simpl; intros H H1; apply interp_full_false; intros H2;
     apply not_not;
     [ apply decidable_correct; assumption
-    | unfold not at 1 in |- *; intro H3; apply hyps_to_goal with (2 := H2);
+    | unfold not at 1; intro H3; apply hyps_to_goal with (2 := H2);
        auto ]
  | intros H1 H2; apply interp_full_false; intro H3;
     elim hyps_to_goal with (1 := H2); assumption ].
@@ -2813,7 +2790,7 @@ Theorem map_cons_val :
  interp_proposition ep e p ->
  interp_list_hyps ep e l -> interp_list_hyps ep e (map_cons _ p l).
 Proof.
- simple induction l; simpl in |- *; [ auto | intros; elim H1; intro H2; auto ].
+ simple induction l; simpl; [ auto | intros; elim H1; intro H2; auto ].
 Qed.
 
 Hint Resolve map_cons_val append_valid decidable_correct.
@@ -2822,43 +2799,43 @@ Theorem destructure_hyps_valid :
  forall n : nat, valid_list_hyps (destructure_hyps n).
 Proof.
  simple induction n;
- [ unfold valid_list_hyps in |- *; simpl in |- *; auto
- | unfold valid_list_hyps at 2 in |- *; intros n1 H ep e lp; case lp;
-    [ simpl in |- *; auto
+ [ unfold valid_list_hyps; simpl; auto
+ | unfold valid_list_hyps at 2; intros n1 H ep e lp; case lp;
+    [ simpl; auto
     | intros p l; case p;
        try
-        (simpl in |- *; intros; apply map_cons_val; simpl in |- *; elim H0;
+        (simpl; intros; apply map_cons_val; simpl; elim H0;
           auto);
        [ intro p'; case p';
           try
-           (simpl in |- *; intros; apply map_cons_val; simpl in |- *; elim H0;
+           (simpl; intros; apply map_cons_val; simpl; elim H0;
              auto);
-          [ simpl in |- *; intros p1 (H1, H2);
-             pattern (decidability p1) in |- *; apply bool_eq_ind;
+          [ simpl; intros p1 (H1, H2);
+             pattern (decidability p1); apply bool_eq_ind;
              intro H3;
-             [ apply H; simpl in |- *; split;
+             [ apply H; simpl; split;
                 [ apply not_not; auto | assumption ]
              | auto ]
-          | simpl in |- *; intros p1 p2 (H1, H2); apply H; simpl in |- *;
+          | simpl; intros p1 p2 (H1, H2); apply H; simpl;
              elim not_or with (1 := H1); auto
-          | simpl in |- *; intros p1 p2 (H1, H2);
-             pattern (decidability p1) in |- *; apply bool_eq_ind;
+          | simpl; intros p1 p2 (H1, H2);
+             pattern (decidability p1); apply bool_eq_ind;
              intro H3;
              [ apply append_valid; elim not_and with (2 := H1);
-                [ intro; left; apply H; simpl in |- *; auto
-                | intro; right; apply H; simpl in |- *; auto
+                [ intro; left; apply H; simpl; auto
+                | intro; right; apply H; simpl; auto
                 | auto ]
              | auto ] ]
-       | simpl in |- *; intros p1 p2 (H1, H2); apply append_valid;
-          (elim H1; intro H3; simpl in |- *; [ left | right ]);
-          apply H; simpl in |- *; auto
-       | simpl in |- *; intros; apply H; simpl in |- *; tauto
-       | simpl in |- *; intros p1 p2 (H1, H2);
-          pattern (decidability p1) in |- *; apply bool_eq_ind;
+       | simpl; intros p1 p2 (H1, H2); apply append_valid;
+          (elim H1; intro H3; simpl; [ left | right ]);
+          apply H; simpl; auto
+       | simpl; intros; apply H; simpl; tauto
+       | simpl; intros p1 p2 (H1, H2);
+          pattern (decidability p1); apply bool_eq_ind;
           intro H3;
           [ apply append_valid; elim imp_simp with (2 := H1);
-             [ intro H4; left; simpl in |- *; apply H; simpl in |- *; auto
-             | intro H4; right; simpl in |- *; apply H; simpl in |- *; auto
+             [ intro H4; left; simpl; apply H; simpl; auto
+             | intro H4; right; simpl; apply H; simpl; auto
              | auto ]
           | auto ] ] ] ].
 Qed.
@@ -2881,8 +2858,8 @@ Theorem p_apply_left_stable :
  forall f : proposition -> proposition,
  prop_stable f -> prop_stable (p_apply_left f).
 Proof.
- unfold prop_stable in |- *; intros f H ep e p; split;
- (case p; simpl in |- *; auto; intros p1; elim (H ep e p1); tauto).
+ unfold prop_stable; intros f H ep e p; split;
+ (case p; simpl; auto; intros p1; elim (H ep e p1); tauto).
 Qed.
 
 Definition p_apply_right (f : proposition -> proposition)
@@ -2899,8 +2876,8 @@ Theorem p_apply_right_stable :
  forall f : proposition -> proposition,
  prop_stable f -> prop_stable (p_apply_right f).
 Proof.
- unfold prop_stable in |- *; intros f H ep e p; split;
- (case p; simpl in |- *; auto;
+ unfold prop_stable; intros f H ep e p; split;
+ (case p; simpl; auto;
    [ intros p1; elim (H ep e p1); tauto
    | intros p1 p2; elim (H ep e p2); tauto
    | intros p1 p2; elim (H ep e p2); tauto
@@ -2923,42 +2900,42 @@ Theorem p_invert_stable :
  forall f : proposition -> proposition,
  prop_stable f -> prop_stable (p_invert f).
 Proof.
- unfold prop_stable in |- *; intros f H ep e p; split;
- (case p; simpl in |- *; auto;
-   [ intros t1 t2; elim (H ep e (NeqTerm t1 t2)); simpl in |- *;
+ unfold prop_stable; intros f H ep e p; split;
+ (case p; simpl; auto;
+   [ intros t1 t2; elim (H ep e (NeqTerm t1 t2)); simpl;
       generalize (dec_eq (interp_term e t1) (interp_term e t2));
-      unfold decidable in |- *; tauto
-   | intros t1 t2; elim (H ep e (GtTerm t1 t2)); simpl in |- *;
+      unfold decidable; tauto
+   | intros t1 t2; elim (H ep e (GtTerm t1 t2)); simpl;
       generalize (dec_gt (interp_term e t1) (interp_term e t2));
-      unfold decidable in |- *; rewrite le_lt_iff, <- gt_lt_iff; tauto
-   | intros t1 t2; elim (H ep e (LtTerm t1 t2)); simpl in |- *;
+      unfold decidable; rewrite le_lt_iff, <- gt_lt_iff; tauto
+   | intros t1 t2; elim (H ep e (LtTerm t1 t2)); simpl;
       generalize (dec_lt (interp_term e t1) (interp_term e t2));
-      unfold decidable in |- *; rewrite ge_le_iff, le_lt_iff; tauto
-   | intros t1 t2; elim (H ep e (LeqTerm t1 t2)); simpl in |- *;
+      unfold decidable; rewrite ge_le_iff, le_lt_iff; tauto
+   | intros t1 t2; elim (H ep e (LeqTerm t1 t2)); simpl;
       generalize (dec_gt (interp_term e t1) (interp_term e t2));
-      unfold decidable in |- *; repeat rewrite le_lt_iff;
+      unfold decidable; repeat rewrite le_lt_iff;
       repeat rewrite gt_lt_iff; tauto
-   | intros t1 t2; elim (H ep e (GeqTerm t1 t2)); simpl in |- *;
+   | intros t1 t2; elim (H ep e (GeqTerm t1 t2)); simpl;
       generalize (dec_lt (interp_term e t1) (interp_term e t2));
-      unfold decidable in |- *; repeat rewrite ge_le_iff;
+      unfold decidable; repeat rewrite ge_le_iff;
       repeat rewrite le_lt_iff; tauto
-   | intros t1 t2; elim (H ep e (EqTerm t1 t2)); simpl in |- *;
+   | intros t1 t2; elim (H ep e (EqTerm t1 t2)); simpl;
       generalize (dec_eq (interp_term e t1) (interp_term e t2));
       unfold decidable; tauto ]).
 Qed.
 
 Theorem move_right_stable : forall s : step, prop_stable (move_right s).
 Proof.
- unfold move_right, prop_stable in |- *; intros s ep e p; split;
- [ Simplify; simpl in |- *; elim (t_rewrite_stable s e); simpl in |- *;
-    [ symmetry  in |- *; apply egal_left; assumption
+ unfold move_right, prop_stable; intros s ep e p; split;
+ [ Simplify; simpl; elim (t_rewrite_stable s e); simpl;
+    [ symmetry ; apply egal_left; assumption
     | intro; apply le_left; assumption
     | intro; apply le_left; rewrite <- ge_le_iff; assumption
     | intro; apply lt_left; rewrite <- gt_lt_iff; assumption
     | intro; apply lt_left; assumption
     | intro; apply ne_left_2; assumption ]
- | case p; simpl in |- *; intros; auto; generalize H; elim (t_rewrite_stable s);
-    simpl in |- *; intro H1;
+ | case p; simpl; intros; auto; generalize H; elim (t_rewrite_stable s);
+    simpl; intro H1;
     [ rewrite (plus_0_r_reverse (interp_term e t0)); rewrite H1;
        rewrite plus_permute; rewrite plus_opp_r;
        rewrite plus_0_r; trivial
@@ -2969,7 +2946,7 @@ Proof.
        rewrite plus_opp_r; assumption
     | rewrite gt_lt_iff; apply lt_left_inv; assumption
     | apply lt_left_inv; assumption
-    | unfold not in |- *; intro H2; apply H1;
+    | unfold not; intro H2; apply H1;
        rewrite H2; rewrite plus_opp_r; trivial ] ].
 Qed.
 
@@ -2985,12 +2962,12 @@ Fixpoint p_rewrite (s : p_step) : proposition -> proposition :=
 
 Theorem p_rewrite_stable : forall s : p_step, prop_stable (p_rewrite s).
 Proof.
- simple induction s; simpl in |- *;
+ simple induction s; simpl;
  [ intros; apply p_apply_left_stable; trivial
  | intros; apply p_apply_right_stable; trivial
  | intros; apply p_invert_stable; apply move_right_stable
  | apply move_right_stable
- | unfold prop_stable in |- *; simpl in |- *; intros; split; auto ].
+ | unfold prop_stable; simpl; intros; split; auto ].
 Qed.
 
 Fixpoint normalize_hyps (l : list h_step) (lh : hyps) {struct l} : hyps :=
@@ -3002,11 +2979,11 @@ Fixpoint normalize_hyps (l : list h_step) (lh : hyps) {struct l} : hyps :=
 Theorem normalize_hyps_valid :
  forall l : list h_step, valid_hyps (normalize_hyps l).
 Proof.
- simple induction l; unfold valid_hyps in |- *; simpl in |- *;
+ simple induction l; unfold valid_hyps; simpl;
  [ auto
  | intros n_s r; case n_s; intros n s H ep e lp H1; apply H;
     apply apply_oper_1_valid;
-    [ unfold valid1 in |- *; intros ep1 e1 p1 H2;
+    [ unfold valid1; intros ep1 e1 p1 H2;
        elim (p_rewrite_stable s ep1 e1 p1); auto
     | assumption ] ].
 Qed.
@@ -3073,21 +3050,21 @@ Theorem extract_valid :
  forall s : list direction,
  valid1 (extract_hyp_pos s) /\ co_valid1 (extract_hyp_neg s).
 Proof.
- unfold valid1, co_valid1 in |- *; simple induction s;
+ unfold valid1, co_valid1; simple induction s;
  [ split;
-    [ simpl in |- *; auto
-    | intros ep e p1; case p1; simpl in |- *; auto; intro p;
-       pattern (decidability p) in |- *; apply bool_eq_ind;
+    [ simpl; auto
+    | intros ep e p1; case p1; simpl; auto; intro p;
+       pattern (decidability p); apply bool_eq_ind;
        [ intro H; generalize (decidable_correct ep e p H);
-          unfold decidable in |- *; tauto
-       | simpl in |- *; auto ] ]
+          unfold decidable; tauto
+       | simpl; auto ] ]
  | intros a s' (H1, H2); simpl in H2; split; intros ep e p; case a; auto;
-    case p; auto; simpl in |- *; intros;
+    case p; auto; simpl; intros;
     (apply H1; tauto) ||
       (apply H2; tauto) ||
-        (pattern (decidability p0) in |- *; apply bool_eq_ind;
+        (pattern (decidability p0); apply bool_eq_ind;
           [ intro H3; generalize (decidable_correct ep e p0 H3);
-             unfold decidable in |- *; intro H4; apply H1;
+             unfold decidable; intro H4; apply H1;
              tauto
           | intro; tauto ]) ].
 Qed.
@@ -3117,29 +3094,29 @@ Fixpoint decompose_solve (s : e_step) (h : hyps) {struct s} : lhyps :=
 Theorem decompose_solve_valid :
  forall s : e_step, valid_list_goal (decompose_solve s).
 Proof.
- intro s; apply goal_valid; unfold valid_list_hyps in |- *; elim s;
- simpl in |- *; intros;
+ intro s; apply goal_valid; unfold valid_list_hyps; elim s;
+ simpl; intros;
  [ cut (interp_proposition ep e1 (extract_hyp_pos l (nth_hyps n lp)));
-    [ case (extract_hyp_pos l (nth_hyps n lp)); simpl in |- *; auto;
-       [ intro p; case p; simpl in |- *; auto; intros p1 p2 H2;
-          pattern (decidability p1) in |- *; apply bool_eq_ind;
+    [ case (extract_hyp_pos l (nth_hyps n lp)); simpl; auto;
+       [ intro p; case p; simpl; auto; intros p1 p2 H2;
+          pattern (decidability p1); apply bool_eq_ind;
           [ intro H3; generalize (decidable_correct ep e1 p1 H3); intro H4;
              apply append_valid; elim H4; intro H5;
-             [ right; apply H0; simpl in |- *; tauto
-             | left; apply H; simpl in |- *; tauto ]
-          | simpl in |- *; auto ]
-       | intros p1 p2 H2; apply append_valid; simpl in |- *; elim H2;
-          [ intros H3; left; apply H; simpl in |- *; auto
-          | intros H3; right; apply H0; simpl in |- *; auto ]
+             [ right; apply H0; simpl; tauto
+             | left; apply H; simpl; tauto ]
+          | simpl; auto ]
+       | intros p1 p2 H2; apply append_valid; simpl; elim H2;
+          [ intros H3; left; apply H; simpl; auto
+          | intros H3; right; apply H0; simpl; auto ]
        | intros p1 p2 H2;
-         pattern (decidability p1) in |- *; apply bool_eq_ind;
+         pattern (decidability p1); apply bool_eq_ind;
           [ intro H3; generalize (decidable_correct ep e1 p1 H3); intro H4;
              apply append_valid; elim H4; intro H5;
-             [ right; apply H0; simpl in |- *; tauto
-             | left; apply H; simpl in |- *; tauto ]
-          | simpl in |- *; auto ] ]
+             [ right; apply H0; simpl; tauto
+             | left; apply H; simpl; tauto ]
+          | simpl; auto ] ]
     | elim (extract_valid l); intros H2 H3; apply H2; apply nth_valid; auto ]
- | intros; apply H; simpl in |- *; split;
+ | intros; apply H; simpl; split;
     [ elim (extract_valid l); intros H2 H3; apply H2; apply nth_valid; auto
     | auto ]
  | apply omega_valid with (1 := H) ].
@@ -3160,11 +3137,11 @@ Fixpoint reduce_lhyps (lp : lhyps) : lhyps :=
 
 Theorem reduce_lhyps_valid : valid_lhyps reduce_lhyps.
 Proof.
- unfold valid_lhyps in |- *; intros ep e lp; elim lp;
- [ simpl in |- *; auto
+ unfold valid_lhyps; intros ep e lp; elim lp;
+ [ simpl; auto
  | intros a l HR; elim a;
-    [ simpl in |- *; tauto
-    | intros a1 l1; case l1; case a1; simpl in |- *; try tauto ] ].
+    [ simpl; tauto
+    | intros a1 l1; case l1; case a1; simpl; try tauto ] ].
 Qed.
 
 Theorem do_reduce_lhyps :
@@ -3184,13 +3161,13 @@ Definition do_concl_to_hyp :
   interp_goal envp env (concl_to_hyp c :: l) ->
   interp_goal_concl c envp env l.
 Proof.
- simpl in |- *; intros envp env c l; induction l as [| a l Hrecl];
- [ simpl in |- *; unfold concl_to_hyp in |- *;
-    pattern (decidability c) in |- *; apply bool_eq_ind;
+ simpl; intros envp env c l; induction l as [| a l Hrecl];
+ [ simpl; unfold concl_to_hyp;
+    pattern (decidability c); apply bool_eq_ind;
     [ intro H; generalize (decidable_correct envp env c H);
-       unfold decidable in |- *; simpl in |- *; tauto
-    | simpl in |- *; intros H1 H2; elim H2; trivial ]
- | simpl in |- *; tauto ].
+       unfold decidable; simpl; tauto
+    | simpl; intros H1 H2; elim H2; trivial ]
+ | simpl; tauto ].
 Qed.
 
 Definition omega_tactic (t1 : e_step) (t2 : list h_step)
@@ -3203,7 +3180,7 @@ Theorem do_omega :
  interp_list_goal envp env (omega_tactic t1 t2 c l) ->
  interp_goal_concl c envp env l.
 Proof.
- unfold omega_tactic in |- *; intros; apply do_concl_to_hyp;
+ unfold omega_tactic; intros; apply do_concl_to_hyp;
  apply (normalize_hyps_goal t2); apply (decompose_solve_valid t1);
  apply do_reduce_lhyps; assumption.
 Qed.