Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part

of the fix I added an optional "by" annotation for rewrite to solve said
conditions in the same tactic call. Most of the theories have been
updated, only FSets is missing, Pierre will take care of it.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10634 85f007b7-540e-0410-9357-904b9bb8a0f7

22 files changed, 230 insertions, 165 deletions

diff --git a/CHANGES b/CHANGES
index e93eb275c..3bba84fc7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -10,7 +10,7 @@ Language
 - New experimental typeclass system giving ad-hoc polymorphism and 
   overloading based on dependent records and implicit arguments.
 - New syntax "let| pat := b in c" for let-binding using irrefutable patterns.
-- New syntax "forall `A`, T" for specifying maximally inserted implicit 
+- New syntax "forall {A}, T" for specifying maximally inserted implicit 
   arguments in terms.
 
 Commands
@@ -139,9 +139,9 @@ Type Classes
 - New theories directory "theories/Classes" for standard typeclasses 
   declarations. Module Classes.Relations is a typeclass port of 
   Relation_Definitions.
-- New experimental "setoid" rewriting tactic "clrewrite" based on typeclasses.
-  Classes.Morphisms declares standard morphisms, Classes.SetoidClasses declares 
-  the new Setoid typeclass.  
+- New experimental "setoid" rewriting tactic based on typeclasses.
+  Classes.Morphisms declares standard morphisms, Classes.Equivalence declares 
+  the new Setoid typeclass and some derived tactics.
   
 Program
 
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index 77d405e15..a0cbe22b3 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -363,7 +363,7 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
     | TacTransitivity c -> depends_of_'constr c acc
 
     (* Equality and inversion *)
-    | TacRewrite (_,cbl,_) -> list_union_map (o depends_of_'constr_with_bindings (fun (_,_,x)->x)) cbl acc
+    | TacRewrite (_,cbl,_,_) -> list_union_map (o depends_of_'constr_with_bindings (fun (_,_,x)->x)) cbl acc
     | TacInversion (is, _)  -> depends_of_'a_'b_inversion_strength depends_of_'constr is acc
 
     (* For ML extensions *)
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 4d28a22a9..c5a8c756a 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1011,14 +1011,15 @@ and xlate_tac =
 		CT_coerce_TACTIC_COM_to_TACTIC_OPT tac
 	in 
 	CT_replace_with (c1, c2,cl,tac_opt)
-    | TacRewrite(false,[b,Precisely 1,cbindl],cl) -> 
+    | TacRewrite(false,[b,Precisely 1,cbindl],cl,None) -> 
      let cl = xlate_clause cl 
      and c = xlate_formula (fst cbindl) 
      and bindl = xlate_bindings (snd cbindl) in
      if b then CT_rewrite_lr (c, bindl, cl)
      else CT_rewrite_rl (c, bindl, cl)
-    | TacRewrite(false,_,cl) -> xlate_error "TODO: rewrite of several hyps at once"
-    | TacRewrite(true,_,cl) -> xlate_error "TODO: erewrite"
+    | TacRewrite(_,_,_,Some _) -> xlate_error "TODO: rewrite by"
+    | TacRewrite(false,_,cl,_) -> xlate_error "TODO: rewrite of several hyps at once"
+    | TacRewrite(true,_,cl,_) -> xlate_error "TODO: erewrite"
     | TacExtend (_,"conditional_rewrite", [t; b; cbindl]) ->
      let t = out_gen rawwit_main_tactic t in
      let b = out_gen Extraargs.rawwit_orient b in
diff --git a/contrib/setoid_ring/Field_theory.v b/contrib/setoid_ring/Field_theory.v
index adaa340db..f5c550417 100644
--- a/contrib/setoid_ring/Field_theory.v
+++ b/contrib/setoid_ring/Field_theory.v
@@ -317,11 +317,12 @@ assert (HH: ~ r5*r6 == 0).
   apply field_is_integral_domain.
     intros H1; case H; rewrite H1; ring.
     intros H1; case H0; rewrite H1; ring.
-rewrite <- rdiv4; auto.
+rewrite <- rdiv4 ; auto.
+  rewrite rdiv_r_r; auto.
+
   apply field_is_integral_domain.
     intros H1; case H; rewrite H1; ring.
     intros H1; case H0; rewrite H1; ring.
-rewrite rdiv_r_r; auto.
 Qed.
 
 
@@ -353,11 +354,11 @@ assert (HH: ~ r5*r6 == 0).
   apply field_is_integral_domain.
     intros H2; case H0; rewrite H2; ring.
     intros H2; case H1; rewrite H2; ring.
-rewrite <- rdiv4; auto.
+rewrite <- rdiv4 ; auto.
+rewrite rdiv_r_r; auto.
   apply field_is_integral_domain.
     intros H2; case H; rewrite H2; ring.
     intros H2; case H0; rewrite H2; ring.
-rewrite rdiv_r_r; auto.
 Qed.
 
 
@@ -379,8 +380,7 @@ transitivity (r1 / r2 * (r4 / r4)).
    rewrite H1 in |- *.
    rewrite (ARmul_comm ARth r2 r4) in |- *.
    rewrite <- rdiv4 in |- *; trivial.
-   rewrite rdiv_r_r in |- *.
-  trivial.
+   rewrite rdiv_r_r in |- * by trivial.
   apply (ARmul_1_r Rsth ARth).
 Qed.
 
@@ -780,7 +780,7 @@ Proof.
   case_eq ((p1 ?= p2)%positive Eq);intros;simpl. 
   repeat rewrite pow_th.(rpow_pow_N);simpl. split. 2:refine (refl_equal _).
   rewrite (Pcompare_Eq_eq _ _ H0).  
-  rewrite H;[trivial | ring [ (morph1 CRmorph)]].
+  rewrite H by trivial. ring [ (morph1 CRmorph)].
   fold (NPEpow e2 (Npos (p2 - p1))).
   rewrite NPEpow_correct;simpl.
   repeat rewrite pow_th.(rpow_pow_N);simpl.
@@ -1048,10 +1048,11 @@ Proof.
  induction p;simpl.
   intro Hp;assert (H1 := @rmul_reg_l _ (pow_pos rmul x p * pow_pos rmul x p) 0 H).
   apply IHp.
-  rewrite (@rmul_reg_l _ (pow_pos rmul x p)  0 IHp). rewrite H1. rewrite Hp;ring. ring.
-  reflexivity. 
+  rewrite (@rmul_reg_l _ (pow_pos rmul x p)  0 IHp). 
+  reflexivity.
+  rewrite H1. ring. rewrite Hp;ring. 
   intro Hp;apply IHp. rewrite (@rmul_reg_l _ (pow_pos rmul x p)  0 IHp).
-  rewrite Hp;ring. reflexivity. trivial.
+  reflexivity. rewrite Hp;ring. trivial.
 Qed.
  
 Theorem Pcond_Fnorm:
@@ -1234,13 +1235,15 @@ generalize (NPEeval l (num (Fnorm e1))) (NPEeval l (denum (Fnorm e1)))
   (Pcond_Fnorm _ _ Hcond).
 intros r r0 Hdiff;induction p;simpl.
 repeat (rewrite <- rdiv4;trivial).
-intro Hp;apply (pow_pos_not_0 Hdiff  p). 
+rewrite IHp. reflexivity.
+apply pow_pos_not_0;trivial.
+apply pow_pos_not_0;trivial.
+intro Hp. apply (pow_pos_not_0 Hdiff  p).
 rewrite  (@rmul_reg_l (pow_pos rmul r0 p) (pow_pos rmul r0 p)  0).
- apply pow_pos_not_0;trivial. ring [Hp]. reflexivity.
-apply pow_pos_not_0;trivial. apply pow_pos_not_0;trivial.
-rewrite IHp;reflexivity.
-rewrite <- rdiv4;trivial. apply pow_pos_not_0;trivial. apply pow_pos_not_0;trivial.
+ reflexivity. apply pow_pos_not_0;trivial. ring [Hp]. 
+rewrite <- rdiv4;trivial. 
 rewrite IHp;reflexivity.
+apply pow_pos_not_0;trivial. apply pow_pos_not_0;trivial.
 reflexivity.
 Qed.
 
@@ -1253,9 +1256,9 @@ Theorem Fnorm_crossproduct:
  PCond l (condition nfe1 ++ condition nfe2) ->
  FEeval l fe1 == FEeval l fe2.
 intros l fe1 fe2 nfe1 nfe2 Hcrossprod Hcond; subst nfe1 nfe2.
-rewrite Fnorm_FEeval_PEeval in |- *.
+rewrite Fnorm_FEeval_PEeval in |- * by
  apply PCond_app_inv_l with (1 := Hcond).
- rewrite Fnorm_FEeval_PEeval in |- *.
+ rewrite Fnorm_FEeval_PEeval in |- * by
   apply PCond_app_inv_r with (1 := Hcond).
   apply cross_product_eq; trivial.
    apply Pcond_Fnorm.
@@ -1473,18 +1476,18 @@ Proof.
  rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe2))));trivial.
  ring [Heq]. rewrite (ARth.(ARmul_comm)  (/ NPEeval l (denum (Fnorm fe2)))).
  repeat rewrite <- (ARth.(ARmul_assoc)).
- rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r. trivial.
+ rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial.
  apply (@rmul_reg_l (/NPEeval l (denum (Fnorm fe1)))).
  intro Heq; apply AFth.(AF_1_neq_0).
  rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe1))));trivial.
  ring [Heq]. repeat rewrite (ARth.(ARmul_comm)  (/ NPEeval l (denum (Fnorm fe1)))).
  repeat rewrite <- (ARth.(ARmul_assoc)).
- repeat rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r. trivial.
+ repeat rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial.
  rewrite (AFth.(AFdiv_def)). ring_simplify. unfold SRopp.
  rewrite  (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe2)))).
  repeat rewrite <- (AFth.(AFdiv_def)).
- repeat rewrite <- Fnorm_FEeval_PEeval;trivial.
- apply (PCond_app_inv_l _ _ _ H7). apply (PCond_app_inv_r _ _ _ H7).
+ repeat rewrite <- Fnorm_FEeval_PEeval ; trivial.
+ apply (PCond_app_inv_r _ _ _ H7). apply (PCond_app_inv_l _ _ _ H7).
 Qed.
 
 Theorem Field_simplify_eq_in_correct :
@@ -1523,18 +1526,18 @@ Proof.
  rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe2))));trivial.
  ring [Heq]. rewrite (ARth.(ARmul_comm)  (/ NPEeval l (denum (Fnorm fe2)))).
  repeat rewrite <- (ARth.(ARmul_assoc)).
- rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r. trivial.
+ rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial.
  apply (@rmul_reg_l (/NPEeval l (denum (Fnorm fe1)))).
  intro Heq; apply AFth.(AF_1_neq_0).
  rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe1))));trivial.
  ring [Heq]. repeat rewrite (ARth.(ARmul_comm)  (/ NPEeval l (denum (Fnorm fe1)))).
  repeat rewrite <- (ARth.(ARmul_assoc)).
- repeat rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r. trivial.
+ repeat rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial.
  rewrite (AFth.(AFdiv_def)). ring_simplify. unfold SRopp.
  rewrite  (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe2)))).
  repeat rewrite <- (AFth.(AFdiv_def)).
  repeat rewrite <- Fnorm_FEeval_PEeval;trivial.
- apply (PCond_app_inv_l _ _ _ H7). apply (PCond_app_inv_r _ _ _ H7).
+ apply (PCond_app_inv_r _ _ _ H7). apply (PCond_app_inv_l _ _ _ H7). 
 Qed.
 
 
diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v
index 56b08a8fa..4d96bec4c 100644
--- a/contrib/setoid_ring/InitialRing.v
+++ b/contrib/setoid_ring/InitialRing.v
@@ -515,12 +515,12 @@ induction x; intros.
 
   simpl Nwadd in |- *.
   repeat rewrite gen_phiNword_cons in |- *.
-  rewrite (fun sreq => gen_phiN_add Rsth sreq (ARth_SRth ARth)) in |- *.
-   destruct Reqe; constructor; trivial.
+  rewrite (fun sreq => gen_phiN_add Rsth sreq (ARth_SRth ARth)) in |- * by
+    (destruct Reqe; constructor; trivial).
 
-   rewrite IHx in |- *.
-   norm.
-   add_push (- gen_phiNword x); reflexivity.
+  rewrite IHx in |- *.
+  norm.
+  add_push (- gen_phiNword x); reflexivity.
 Qed.
 
 Lemma Nwopp_ok : forall x, gen_phiNword (Nwopp x) == - gen_phiNword x.
@@ -537,8 +537,8 @@ induction x; intros.
 
  simpl Nwscal in |- *.
  repeat rewrite gen_phiNword_cons in |- *.
- rewrite (fun sreq => gen_phiN_mult Rsth sreq (ARth_SRth ARth)) in |- *.
-  destruct Reqe; constructor; trivial.
+ rewrite (fun sreq => gen_phiN_mult Rsth sreq (ARth_SRth ARth)) in |- *
+   by (destruct Reqe; constructor; trivial).
 
   rewrite IHx in |- *.
   norm.
diff --git a/contrib/setoid_ring/Ring_polynom.v b/contrib/setoid_ring/Ring_polynom.v
index 70199676c..45b38e2ed 100644
--- a/contrib/setoid_ring/Ring_polynom.v
+++ b/contrib/setoid_ring/Ring_polynom.v
@@ -1064,7 +1064,7 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
    rewrite Padd_ok; rewrite PmulC_ok; rsimpl.
  intros i P5 H; rewrite H.
    intros HH H1; injection HH; intros; subst; rsimpl.
-   rewrite Padd_ok; rewrite PmulI_ok. intros;apply Pmul_ok. rewrite H1; rsimpl.
+   rewrite Padd_ok; rewrite PmulI_ok by (intros;apply Pmul_ok). rewrite H1; rsimpl. 
  intros i P5 P6 H1 H2 H3; rewrite H1; rewrite H3.
    assert (P4 = Q1 ++ P3 ** PX i P5 P6).
    injection H2; intros; subst;trivial.
@@ -1258,7 +1258,7 @@ Section POWER.
  
   Lemma Ppow_N_ok : forall l,  (forall P, subst_l P@l == P@l) ->
          forall P n, (Ppow_N P n)@l == (pow_N P1 Pmul P n)@l.
-  Proof.  destruct n;simpl. rrefl. rewrite Ppow_pos_ok. trivial. Esimpl.  Qed.
+  Proof.  destruct n;simpl. rrefl. rewrite Ppow_pos_ok by trivial. Esimpl.  Qed.
     
  End POWER.
 
@@ -1334,7 +1334,7 @@ Section POWER.
    rewrite IHpe1;rewrite IHpe2;rrefl.
    rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. rrefl.
    rewrite IHpe;rrefl.
-   rewrite Ppow_N_ok. intros;rrefl.
+   rewrite Ppow_N_ok by (intros;rrefl).
    rewrite pow_th.(rpow_pow_N). destruct n0;Esimpl3.
    induction p;simpl;try rewrite IHp;try rewrite IHpe;repeat rewrite Pms_ok; 
       repeat rewrite Pmul_ok;rrefl.
@@ -1425,7 +1425,7 @@ Section POWER.
    assert (HH:=mon_of_pol_ok (norm_subst 0 nil  p));
      destruct  (mon_of_pol (norm_subst 0 nil p)).  
    split.
-   rewrite <- norm_subst_spec. exact I.
+   rewrite <- norm_subst_spec by exact I.
    destruct lpe;try destruct H;rewrite <- H;
    rewrite (norm_subst_spec 0 nil); try exact I;apply HH;trivial.
    apply IHlpe. destruct lpe;simpl;trivial. destruct H. exact H0.
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index a4e5d4cb8..96db00e3e 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -319,6 +319,10 @@ GEXTEND Gram
     [ [ IDENT "by"; tac = tactic_expr LEVEL "3" -> TacComplete tac
       | -> TacId [] ] ]
   ;
+  opt_by_tactic:
+    [ [ IDENT "by"; tac = tactic_expr LEVEL "3" -> Some tac
+    | -> None ] ]
+  ;
   rename : 
     [ [ id1 = id_or_meta; IDENT "into"; id2 = id_or_meta -> (id1,id2) ] ]
   ;
@@ -471,10 +475,10 @@ GEXTEND Gram
       | IDENT "transitivity"; c = constr -> TacTransitivity c
 
       (* Equality and inversion *)
-      | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause ->
-	  TacRewrite (false,l,cl)
-      | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause ->
-	  TacRewrite (true,l,cl)
+      | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause; t=opt_by_tactic ->
+	  TacRewrite (false,l,cl,t)
+      | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause; t=opt_by_tactic ->
+	  TacRewrite (true,l,cl,t)
       | IDENT "dependent"; k =
 	  [ IDENT "simple"; IDENT "inversion" -> SimpleInversion
 	  | IDENT "inversion" -> FullInversion
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index da915a5cc..448b78e26 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -821,14 +821,15 @@ and pr_atom1 = function
   | TacTransitivity c -> str "transitivity" ++ pr_constrarg c
 
   (* Equality and inversion *)
-  | TacRewrite (ev,l,cl) -> 
+  | TacRewrite (ev,l,cl,by) -> 
       hov 1 (str (if ev then "erewrite" else "rewrite") ++ 
 	     prlist_with_sep
 	     (fun () -> str ","++spc())
 	     (fun (b,m,c) -> 
 		pr_orient b ++ spc() ++ pr_multi m ++ pr_with_bindings c)
 	     l
-	     ++ pr_clauses pr_ident cl) 
+	     ++ pr_clauses pr_ident cl
+	     ++	(match by with Some by -> pr_by_tactic (pr_tac_level ltop) by | None -> mt())) 
   | TacInversion (DepInversion (k,c,ids),hyp) ->
       hov 1 (str "dependent " ++ pr_induction_kind k ++ spc () ++
       pr_quantified_hypothesis hyp ++
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index a63fd1aeb..f74413704 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -194,7 +194,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
 
   (* Equality and inversion *)
   | TacRewrite of 
-      evars_flag * (bool * multi * 'constr with_bindings) list * 'id gclause
+      evars_flag * (bool * multi * 'constr with_bindings) list * 'id gclause * 'tac option
   | TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis
       
   (* For ML extensions *)
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 193f0966e..bb73d4094 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -516,6 +516,33 @@ let resolve_morphism env sigma oldt m args args' cstr evars =
 	[ a, r ] -> (proof, (a, r, oldt, newt))
       | _ -> assert(false)
 
+(* Adapted from setoid_replace. *)
+
+type hypinfo = {
+  cl : clausenv;
+  prf : constr;
+  rel : constr;
+  l2r : bool;
+  c1 : constr;
+  c2 : constr;
+  c  : constr option;
+  abs : (constr * types) option;
+}
+
+let decompose_setoid_eqhyp gl c left2right =
+  let ctype = pf_type_of gl c in
+  let eqclause  = Clenv.make_clenv_binding gl (c,ctype) Rawterm.NoBindings in
+  let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
+  let rec split_last_two = function
+    | [c1;c2] -> [],(c1, c2)
+    | x::y::z ->
+	let l,res = split_last_two (y::z) in x::l, res
+    | _ -> error "The term provided is not an applied relation" in
+  let others, (c1,c2) = split_last_two args in
+    { cl=eqclause; prf=(Clenv.clenv_value eqclause);
+      rel=mkApp (equiv, Array.of_list others);
+      l2r=left2right; c1=c1; c2=c2; c=Some c; abs=None }
+
 let rewrite_unif_flags = {
   Unification.modulo_conv_on_closed_terms = false;
   Unification.use_metas_eagerly = true;
@@ -549,8 +576,9 @@ let rewrite2_unif_flags = {
 
 let allowK = true
 
-let unify_eqn gl (cl, rel, l2r, c1, c2) t = 
+let unify_eqn gl hypinfo t = 
   try 
+    let {cl=cl; prf=prf; rel=rel; l2r=l2r; c1=c1; c2=c2; c=c; abs=abs} = !hypinfo in
     let env' = 
       try clenv_unify allowK ~flags:rewrite_unif_flags
 	CONV (if l2r then c1 else c2) t cl
@@ -559,14 +587,26 @@ let unify_eqn gl (cl, rel, l2r, c1, c2) t =
 	  CONV (if l2r then c1 else c2) t cl
     in
     let c1 = Clenv.clenv_nf_meta env' c1 
-    and c2 = Clenv.clenv_nf_meta env' c2 
-    and typ = Clenv.clenv_type env' in
-    let (rel, args) = destApp typ in
-    let relargs, args = array_chop (Array.length args - 2) args in
-    let rel = mkApp (rel, relargs) in
+    and c2 = Clenv.clenv_nf_meta env' c2
+    and rel = Clenv.clenv_nf_meta env' rel in
     let car = pf_type_of gl c1 in
-    let prf = Clenv.clenv_value env' in
-    let res = 
+    let prf =
+      if abs = None then
+(* 	let (rel, args) = destApp typ in *)
+(* 	let relargs, args = array_chop (Array.length args - 2) args in *)
+(* 	let rel = mkApp (rel, relargs) in *)
+	let prf = Clenv.clenv_value env' in
+	  begin
+	    match c with 
+	      | Some c when occur_meta prf ->
+		  (* Refresh the clausenv to not get the same meta twice in the goal. *)
+		  hypinfo := decompose_setoid_eqhyp gl c l2r;
+	      | _ -> ()
+	  end;
+	  prf
+      else prf
+    in
+    let res =
       if l2r then (prf, (car, rel, c1, c2))
       else
 	try (mkApp (symmetric_proof (pf_env gl) car rel, [| c1 ; c2 ; prf |]), (car, rel, c2, c1))
@@ -626,25 +666,11 @@ let build_new gl env sigma occs hypinfo concl cstr evars =
 	    | _ -> None, occ
   in aux concl 1 cstr
     
-(* Adapted from setoid_replace. *)
-
-let decompose_setoid_eqhyp gl c left2right =
-  let ctype = pf_type_of gl c in
-  let eqclause  = Clenv.make_clenv_binding gl (c,ctype) Rawterm.NoBindings in
-  let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
-  let rec split_last_two = function
-    | [c1;c2] -> [],(c1, c2)
-    | x::y::z ->
-	let l,res = split_last_two (y::z) in x::l, res
-    | _ -> error "The term provided is not an applied relation" in
-  let others, (c1,c2) = split_last_two args in
-    eqclause, mkApp (equiv, Array.of_list others), left2right, c1, c2
-
 let resolve_all_typeclasses env evd = 
   resolve_all_evars false (true, 15) env
     (fun ev evi -> Typeclasses.class_of_constr evi.Evd.evar_concl <> None) evd
     
-let cl_rewrite_clause_aux hypinfo occs clause gl =
+let cl_rewrite_clause_aux hypinfo goal_meta occs clause gl =
   let concl, is_hyp = 
     match clause with
 	Some ((_, id), _) -> pf_get_hyp_typ gl id, Some id
@@ -670,17 +696,26 @@ let cl_rewrite_clause_aux hypinfo occs clause gl =
 	      let rewtac, cleantac = 
 		match is_hyp with
 		  | Some id -> 
-(* 		      let meta = Evarutil.new_meta() in *)
-(* 		      let term = mkApp (p, [| mkCast (mkMeta meta, DEFAULTcast, newt) |]) in *)
-(* 		      tclTHEN *)
-(* 			(tclEVARS (evars_of clenv.evd)) *)
-		      cut_replacing id newt (fun x ->
-			refine (mkApp (p, [| mkVar id |]))),
+		      let term = 
+			match !hypinfo.abs with
+			    None -> p
+			  | Some (t, ty) -> 
+			      mkApp (mkLambda (Name (id_of_string "lemma"), ty, p), [| t |])
+		      in
+			cut_replacing id newt 
+			  (fun x -> Tactics.refine (mkApp (term, [| mkVar id |]))),
 		      unfold_in_hyp unfoldrefs (([], id), Tacexpr.InHyp)
 		  | None -> 
-		      let meta = Evarutil.new_meta() in
-		      let term = mkApp (p, [| mkCast (mkMeta meta, DEFAULTcast, newt) |]) in
-			refine term, Tactics.unfold_in_concl unfoldrefs
+(* 		      let term = mkApp (p, [| mkCast (mkMeta goal_meta, DEFAULTcast, newt) |]) in *)
+		      let term = match !hypinfo.abs with
+			  None -> mkApp (p, [| mkCast (mkMeta goal_meta, DEFAULTcast, newt) |])
+			| Some (t, ty) -> 
+			    mkApp (mkLambda (Name (id_of_string "newt"), newt,
+					    mkLambda (Name (id_of_string "lemma"), ty,
+						     mkApp (p, [| mkRel 2 |]))),
+				  [| mkMeta goal_meta; t |])
+		      in
+			Tactics.refine term, Tactics.unfold_in_concl unfoldrefs
 	      in
 	      let evartac = 
 		let evd = Evd.evars_of undef in
@@ -690,13 +725,14 @@ let cl_rewrite_clause_aux hypinfo occs clause gl =
 	    with UserError (env, e) -> 
 	      tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints") gl)
       | None -> 
-	  let (_, _, l2r, x, y) = hypinfo in
+	  let {l2r=l2r; c1=x; c2=y} = !hypinfo in
 	    raise (Pretype_errors.PretypeError (pf_env gl, Pretype_errors.NoOccurrenceFound (if l2r then x else y)))
 	      (* tclFAIL 1 (str"setoid rewrite failed") gl *)
 	  
 let cl_rewrite_clause c left2right occs clause gl =
-  let hypinfo = decompose_setoid_eqhyp gl c left2right in
-    cl_rewrite_clause_aux hypinfo occs clause gl
+  let meta = Evarutil.new_meta() in
+  let hypinfo = ref (decompose_setoid_eqhyp gl c left2right) in
+    cl_rewrite_clause_aux hypinfo meta occs clause gl
 
 open Genarg
 open Extraargs
@@ -1021,8 +1057,6 @@ let default_morphism sign m =
     	  
 let unfold_respectful = lazy (Tactics.unfold_in_concl [[], EvalConstRef (destConst (Lazy.force respectful))])
 
-let ($) g f = fun x -> g (f x)
-
 VERNAC COMMAND EXTEND AddSetoid1
    [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
      [	init_setoid ();
@@ -1082,7 +1116,26 @@ END
 (** Taken from original setoid_replace, to emulate the old rewrite semantics where
     lemmas are first instantiated once and then rewrite proceeds. *)
 
-let unification_rewrite l2r c1 c2 cl but gl = 
+let check_evar_map_of_evars_defs evd =
+ let metas = Evd.meta_list evd in
+ let check_freemetas_is_empty rebus =
+  Evd.Metaset.iter
+   (fun m ->
+     if Evd.meta_defined evd m then () else
+      raise (Logic.RefinerError (Logic.OccurMetaGoal rebus)))
+ in
+  List.iter
+   (fun (_,binding) ->
+     match binding with
+        Evd.Cltyp (_,{Evd.rebus=rebus; Evd.freemetas=freemetas}) ->
+         check_freemetas_is_empty rebus freemetas
+      | Evd.Clval (_,({Evd.rebus=rebus1; Evd.freemetas=freemetas1},_),
+                 {Evd.rebus=rebus2; Evd.freemetas=freemetas2}) ->
+         check_freemetas_is_empty rebus1 freemetas1 ;
+         check_freemetas_is_empty rebus2 freemetas2
+   ) metas
+
+let unification_rewrite l2r c1 c2 cl rel but gl = 
   let (env',c') =
     try
       (* ~flags:(false,true) to allow to mark occurences that must not be
@@ -1099,23 +1152,31 @@ let unification_rewrite l2r c1 c2 cl but gl =
   let cl' = {cl with evd = env' } in
   let c1 = Clenv.clenv_nf_meta cl' c1 
   and c2 = Clenv.clenv_nf_meta cl' c2 in
-    cl', Clenv.clenv_value cl', l2r, c1, c2
+  check_evar_map_of_evars_defs env';
+  let prf = Clenv.clenv_value cl' in
+  let prfty = Clenv.clenv_type cl' in
+    if occur_meta prf then
+      {cl=cl'; prf=(mkRel 1); rel=rel; l2r=l2r; c1=c1; c2=c2; c=None; abs=Some (prf, prfty)}
+    else
+      {cl=cl'; prf=prf; rel=rel; l2r=l2r; c1=c1; c2=c2; c=None; abs=None}
 
 let get_hyp gl c clause l2r = 
   match kind_of_term (pf_type_of gl c) with
       Prod _ -> 
-	let cl, rel, _, c1, c2 = decompose_setoid_eqhyp gl c l2r in
+	let hi = decompose_setoid_eqhyp gl c l2r in
 	let but = match clause with Some id -> pf_get_hyp_typ gl id | None -> pf_concl gl in
-	  unification_rewrite l2r c1 c2 cl but gl 
+	  unification_rewrite hi.l2r hi.c1 hi.c2 hi.cl hi.rel but gl
     | _ -> decompose_setoid_eqhyp gl c l2r
 	
 let general_s_rewrite l2r c ~new_goals gl =
-  let hypinfo = get_hyp gl c None l2r in
-    cl_rewrite_clause_aux hypinfo [] None gl
+  let meta = Evarutil.new_meta() in
+  let hypinfo = ref (get_hyp gl c None l2r) in
+    cl_rewrite_clause_aux hypinfo meta [] None gl
 
 let general_s_rewrite_in id l2r c ~new_goals gl =
-  let hypinfo = get_hyp gl c (Some id) l2r in
-    cl_rewrite_clause_aux hypinfo [] (Some (([],id), [])) gl
+  let meta = Evarutil.new_meta() in
+  let hypinfo = ref (get_hyp gl c (Some id) l2r) in
+    cl_rewrite_clause_aux hypinfo meta [] (Some (([],id), [])) gl
     
 let general_s_rewrite_clause = function
   | None -> general_s_rewrite
@@ -1215,15 +1276,3 @@ END
 (* TACTIC EXTEND class_apply *)
 (*     | [ "class_apply" constr_with_bindings(t) ] -> [ class_apply t ] *)
 (* END *)
-
-(* let default_morphism ?(filter=fun _ -> true) m = *)
-(*   match List.filter filter (morphism_table_find m) with *)
-(*       [] -> raise Not_found *)
-(*     | m1::ml -> *)
-(*         if ml <> [] then *)
-(*           Flags.if_warn msg_warning *)
-(*             (strbrk "There are several morphisms associated to \"" ++ *)
-(*             pr_lconstr m ++ strbrk "\". Morphism " ++ prmorphism m m1 ++ *)
-(*             strbrk " is randomly chosen."); *)
-(*         relation_morphism_of_constr_morphism m1 *)
-
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 93b555b34..214389f18 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -175,8 +175,13 @@ let general_multi_rewrite l2r with_evars c cl =
 	      (general_rewrite_ebindings l2r c with_evars)
 	      do_hyps
 
-let general_multi_multi_rewrite with_evars l cl = 
-  let do1 l2r c = general_multi_rewrite l2r with_evars c cl in
+let general_multi_multi_rewrite with_evars l cl tac = 
+  let do1 l2r c = 
+    match tac with
+	None -> general_multi_rewrite l2r with_evars c cl
+      | Some tac -> tclTHENSFIRSTn (general_multi_rewrite l2r with_evars c cl)
+	  [|tclIDTAC|] (tclCOMPLETE tac)
+  in
   let rec doN l2r c = function 
     | Precisely n when n <= 0 -> tclIDTAC
     | Precisely 1 -> do1 l2r c
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 846487f96..91a0d33c6 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -53,7 +53,8 @@ val general_rewrite_in          :
 val general_multi_rewrite : 
   bool -> evars_flag -> constr with_ebindings -> clause -> tactic
 val general_multi_multi_rewrite : 
-  evars_flag -> (bool * multi * constr with_ebindings) list -> clause -> tactic
+  evars_flag -> (bool * multi * constr with_ebindings) list -> clause -> 
+  tactic option -> tactic
 
 val conditional_rewrite : bool -> tactic -> constr with_ebindings -> tactic
 val conditional_rewrite_in :
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 8de4fcd10..3245c31c7 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -742,11 +742,12 @@ let rec intern_atomic lf ist x =
   | TacTransitivity c -> TacTransitivity (intern_constr ist c)
 
   (* Equality and inversion *)
-  | TacRewrite (ev,l,cl) -> 
+  | TacRewrite (ev,l,cl,by) -> 
       TacRewrite 
 	(ev, 
-	 List.map (fun (b,m,c) -> (b,m,intern_constr_with_bindings ist c)) l,
-	 clause_app (intern_hyp_location ist) cl)
+	List.map (fun (b,m,c) -> (b,m,intern_constr_with_bindings ist c)) l,
+	clause_app (intern_hyp_location ist) cl,
+	Option.map (intern_tactic ist) by)
   | TacInversion (inv,hyp) ->
       TacInversion (intern_inversion_strength lf ist inv,
         intern_quantified_hypothesis ist hyp)
@@ -2105,10 +2106,11 @@ and interp_atomic ist gl = function
   | TacTransitivity c -> h_transitivity (pf_interp_constr ist gl c)
 
   (* Equality and inversion *)
-  | TacRewrite (ev,l,cl) -> 
+  | TacRewrite (ev,l,cl,by) -> 
       Equality.general_multi_multi_rewrite ev
 	(List.map (fun (b,m,c) -> (b,m,interp_constr_with_bindings ist gl c)) l)
 	(interp_clause ist gl cl)
+	(Option.map (interp_tactic ist) by)
   | TacInversion (DepInversion (k,c,ids),hyp) ->
       Inv.dinv k (Option.map (pf_interp_constr ist gl) c)
         (interp_intro_pattern ist gl ids)
@@ -2403,11 +2405,11 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacTransitivity c -> TacTransitivity (subst_rawconstr subst c)
 
   (* Equality and inversion *)
-  | TacRewrite (ev,l,cl) -> 
+  | TacRewrite (ev,l,cl,by) -> 
       TacRewrite (ev, 
 		  List.map (fun (b,m,c) ->
 			      b,m,subst_raw_with_bindings subst c) l,
-		  cl)
+		 cl,Option.map (subst_tactic subst) by)
   | TacInversion (DepInversion (k,c,l),hyp) ->
      TacInversion (DepInversion (k,Option.map (subst_rawconstr subst) c,l),hyp)
   | TacInversion (NonDepInversion _,_) as x -> x
diff --git a/theories/Ints/num/QvMake.v b/theories/Ints/num/QvMake.v
index e51291a04..c3db44bc6 100644
--- a/theories/Ints/num/QvMake.v
+++ b/theories/Ints/num/QvMake.v
@@ -429,8 +429,8 @@ Module Qv.
  Theorem spec_sub x y: wf x -> wf y ->
   ([sub x y] == [x] - [y])%Q.
  intros x y Hx Hy; unfold sub; rewrite spec_add; auto.
- apply wf_opp; auto.
  rewrite spec_opp; ring.
+ apply wf_opp; auto.
  Qed.
 
  Theorem spec_subc x y: wf x -> wf y ->
@@ -450,8 +450,8 @@ Module Qv.
  Theorem spec_sub_norm x y: wf x -> wf y ->
   ([sub_norm x y] == [x] - [y])%Q.
  intros x y Hx Hy; unfold sub_norm; rewrite spec_add_norm; auto.
- apply wf_opp; auto.
  rewrite spec_opp; ring.
+ apply wf_opp; auto.
  Qed.
 
  Theorem spec_sub_normc x y: wf x -> wf y ->
@@ -945,10 +945,10 @@ Module Qv.
  Theorem spec_div x y: wf x -> wf y ->
   ([div x y] == [x] / [y])%Q.
  intros x y Hx Hy; unfold div; rewrite spec_mul; auto.
- apply wf_inv; auto.
  unfold Qdiv; apply Qmult_comp.
  apply Qeq_refl.
  apply spec_inv; auto.
+ apply wf_inv; auto.
  Qed.
 
  Theorem spec_divc x y: wf x -> wf y ->
@@ -969,10 +969,10 @@ Module Qv.
  Theorem spec_div_norm x y: wf x -> wf y ->
   ([div_norm x y] == [x] / [y])%Q.
  intros x y Hx Hy; unfold div_norm; rewrite spec_mul_norm; auto.
- apply wf_inv; auto.
  unfold Qdiv; apply Qmult_comp.
  apply Qeq_refl.
  apply spec_inv; auto.
+ apply wf_inv; auto.
  Qed.
 
  Theorem spec_div_normc x y: wf x -> wf y ->
diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v
index 36a845824..f0751f670 100644
--- a/theories/NArith/BinPos.v
+++ b/theories/NArith/BinPos.v
@@ -802,7 +802,7 @@ Qed.
 Theorem Pcompare_Eq_eq : forall p q:positive, (p ?= q) Eq = Eq -> p = q.
 Proof.
   intro x; induction x as [p IHp| p IHp| ]; intro y; destruct y as [q| q| ];
-    simpl in |- *; auto; intro H;
+    simpl in |- *; auto; intro H ;
       [ rewrite (IHp q); trivial
         | absurd ((p ?= q) Gt = Eq);
           [ elim (Pcompare_not_Eq p q); auto | assumption ]
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index fc9115e20..a40832507 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -210,8 +210,9 @@ destruct n as [n m].
 cut (forall p : N, A (p, 0)); [intro H1 |].
 cut (forall p : N, A (0, p)); [intro H2 |].
 destruct (plus_dichotomy n m) as [[p H] | [p H]].
-rewrite (A_wd (n, m) (0, p)); simpl. rewrite plus_0_l; now rewrite plus_comm. apply H2.
-rewrite (A_wd (n, m) (p, 0)); simpl. now rewrite plus_0_r. apply H1.
+rewrite (A_wd (n, m) (0, p)) by (rewrite plus_0_l; now rewrite plus_comm).
+apply H2.
+rewrite (A_wd (n, m) (p, 0)) by now rewrite plus_0_r. apply H1.
 induct p. assumption. intros p IH.
 apply -> (A_wd (0, p) (1, S p)) in IH; [| now rewrite plus_0_l, plus_1_l].
 now apply <- AS.
@@ -302,13 +303,13 @@ Add Morphism NZmin with signature Zeq ==> Zeq ==> Zeq as NZmin_wd.
 Proof.
 intros n1 m1 H1 n2 m2 H2; unfold NZmin, Zeq; simpl.
 destruct (le_ge_cases (fst n1 + snd n2) (fst n2 + snd n1)) as [H | H].
-rewrite (min_l (fst n1 + snd n2) (fst n2 + snd n1)). assumption.
-rewrite (min_l (fst m1 + snd m2) (fst m2 + snd m1)).
+rewrite (min_l (fst n1 + snd n2) (fst n2 + snd n1)) by assumption.
+rewrite (min_l (fst m1 + snd m2) (fst m2 + snd m1)) by
 now apply -> (NZle_wd n1 m1 H1 n2 m2 H2).
 stepl ((fst n1 + snd m1) + (snd n2 + snd m2)) by ring.
 unfold Zeq in H1. rewrite H1. ring.
-rewrite (min_r (fst n1 + snd n2) (fst n2 + snd n1)). assumption.
-rewrite (min_r (fst m1 + snd m2) (fst m2 + snd m1)).
+rewrite (min_r (fst n1 + snd n2) (fst n2 + snd n1)) by assumption.
+rewrite (min_r (fst m1 + snd m2) (fst m2 + snd m1)) by
 now apply -> (NZle_wd n2 m2 H2 n1 m1 H1).
 stepl ((fst n2 + snd m2) + (snd n1 + snd m1)) by ring.
 unfold Zeq in H2. rewrite H2. ring.
@@ -318,13 +319,13 @@ Add Morphism NZmax with signature Zeq ==> Zeq ==> Zeq as NZmax_wd.
 Proof.
 intros n1 m1 H1 n2 m2 H2; unfold NZmax, Zeq; simpl.
 destruct (le_ge_cases (fst n1 + snd n2) (fst n2 + snd n1)) as [H | H].
-rewrite (max_r (fst n1 + snd n2) (fst n2 + snd n1)). assumption.
-rewrite (max_r (fst m1 + snd m2) (fst m2 + snd m1)).
+rewrite (max_r (fst n1 + snd n2) (fst n2 + snd n1)) by assumption.
+rewrite (max_r (fst m1 + snd m2) (fst m2 + snd m1)) by
 now apply -> (NZle_wd n1 m1 H1 n2 m2 H2).
 stepl ((fst n2 + snd m2) + (snd n1 + snd m1)) by ring.
 unfold Zeq in H2. rewrite H2. ring.
-rewrite (max_l (fst n1 + snd n2) (fst n2 + snd n1)). assumption.
-rewrite (max_l (fst m1 + snd m2) (fst m2 + snd m1)).
+rewrite (max_l (fst n1 + snd n2) (fst n2 + snd n1)) by assumption.
+rewrite (max_l (fst m1 + snd m2) (fst m2 + snd m1)) by
 now apply -> (NZle_wd n2 m2 H2 n1 m1 H1).
 stepl ((fst n1 + snd m1) + (snd n2 + snd m2)) by ring.
 unfold Zeq in H1. rewrite H1. ring.
@@ -350,25 +351,25 @@ Qed.
 Theorem NZmin_l : forall n m : Z, n <= m -> Zmin n m == n.
 Proof.
 unfold Zmin, Zle, Zeq; simpl; intros n m H.
-rewrite min_l. assumption. ring.
+rewrite min_l by assumption. ring.
 Qed.
 
 Theorem NZmin_r : forall n m : Z, m <= n -> Zmin n m == m.
 Proof.
 unfold Zmin, Zle, Zeq; simpl; intros n m H.
-rewrite min_r. assumption. ring.
+rewrite min_r by assumption. ring.
 Qed.
 
 Theorem NZmax_l : forall n m : Z, m <= n -> Zmax n m == n.
 Proof.
 unfold Zmax, Zle, Zeq; simpl; intros n m H.
-rewrite max_l. assumption. ring.
+rewrite max_l by assumption. ring.
 Qed.
 
 Theorem NZmax_r : forall n m : Z, n <= m -> Zmax n m == m.
 Proof.
 unfold Zmax, Zle, Zeq; simpl; intros n m H.
-rewrite max_r. assumption. ring.
+rewrite max_r by assumption. ring.
 Qed.
 
 End NZOrdAxiomsMod.
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index bc3600f9c..133bbde4d 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -140,11 +140,12 @@ setoid_replace (n < n) with False using relation iff by
 now setoid_replace (S n <= n) with False using relation iff by
   (apply -> neg_false; apply NZnle_succ_diag_l).
 intro m. rewrite NZlt_succ_r. rewrite NZle_succ_r.
-rewrite NZsucc_inj_wd. rewrite (NZlt_eq_cases n m).
+rewrite NZsucc_inj_wd.
+rewrite (NZlt_eq_cases n m).
 rewrite or_cancel_r.
+reflexivity.
 intros H1 H2; rewrite H2 in H1; false_hyp H1 NZnle_succ_diag_l.
 apply NZlt_neq.
-reflexivity.
 Qed.
 
 Theorem NZlt_succ_l : forall n m : NZ, S n < m -> n < m.
diff --git a/theories/Numbers/NatInt/NZTimesOrder.v b/theories/Numbers/NatInt/NZTimesOrder.v
index 51d2172de..b51e3d22b 100644
--- a/theories/Numbers/NatInt/NZTimesOrder.v
+++ b/theories/Numbers/NatInt/NZTimesOrder.v
@@ -60,7 +60,7 @@ split; [apply LR |]. intro H2. apply -> NZlt_dne; intro H3.
 apply <- NZle_ngt in H3. le_elim H3.
 apply NZlt_asymm in H2. apply H2. now apply LR.
 rewrite H3 in H2; false_hyp H2 NZlt_irrefl.
-rewrite (NZtimes_lt_pred p (S p)); [reflexivity |].
+rewrite (NZtimes_lt_pred p (S p)) by reflexivity.
 rewrite H; do 2 rewrite NZtimes_0_l; now do 2 rewrite NZplus_0_l.
 Qed.
 
@@ -109,9 +109,9 @@ assert (H4 : p * n < p * m); [now apply -> NZtimes_lt_mono_neg_l |].
 rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
 false_hyp H2 H.
 apply -> NZeq_dne; intro H3. apply -> NZlt_gt_cases in H3. destruct H3 as [H3 | H3].
-assert (H4 : p * n < p * m); [now apply -> NZtimes_lt_mono_pos_l |].
+assert (H4 : p * n < p * m) by (now apply -> NZtimes_lt_mono_pos_l).
 rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
-assert (H4 : p * m < p * n); [now apply -> NZtimes_lt_mono_pos_l |].
+assert (H4 : p * m < p * n) by (now apply -> NZtimes_lt_mono_pos_l).
 rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
 now rewrite H1.
 Qed.
@@ -135,9 +135,9 @@ Qed.
 Theorem NZtimes_le_mono_pos_l : forall n m p : NZ, 0 < p -> (n <= m <-> p * n <= p * m).
 Proof.
 intros n m p H; do 2 rewrite NZlt_eq_cases.
-rewrite (NZtimes_lt_mono_pos_l p n m); [assumption |].
-now rewrite -> (NZtimes_cancel_l n m p);
-[intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl |].
+rewrite (NZtimes_lt_mono_pos_l p n m) by assumption.
+now rewrite -> (NZtimes_cancel_l n m p) by
+(intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl).
 Qed.
 
 Theorem NZtimes_le_mono_pos_r : forall n m p : NZ, 0 < p -> (n <= m <-> n * p <= m * p).
@@ -149,9 +149,8 @@ Qed.
 Theorem NZtimes_le_mono_neg_l : forall n m p : NZ, p < 0 -> (n <= m <-> p * m <= p * n).
 Proof.
 intros n m p H; do 2 rewrite NZlt_eq_cases.
-rewrite (NZtimes_lt_mono_neg_l p n m); [assumption |].
-rewrite -> (NZtimes_cancel_l m n p);
-[intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl |].
+rewrite (NZtimes_lt_mono_neg_l p n m); [| assumption].
+rewrite -> (NZtimes_cancel_l m n p) by (intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl).
 now setoid_replace (n == m) with (m == n) using relation iff by (split; now intro).
 Qed.
 
diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v
index 10c341cbf..4df46e20e 100644
--- a/theories/Numbers/Natural/Abstract/NIso.v
+++ b/theories/Numbers/Natural/Abstract/NIso.v
@@ -51,8 +51,8 @@ Theorem natural_isomorphism_succ :
   forall n : N1, natural_isomorphism (S1 n) == S2 (natural_isomorphism n).
 Proof.
 unfold natural_isomorphism.
-intro n. now rewrite (@NAxiomsMod1.recursion_succ N2 NAxiomsMod2.Neq);
-[| unfold fun2_wd; intros; apply NBasePropMod2.succ_wd |].
+intro n. now rewrite (@NAxiomsMod1.recursion_succ N2 NAxiomsMod2.Neq) ;
+[ | | unfold fun2_wd; intros; apply NBasePropMod2.succ_wd].
 Qed.
 
 Theorem hom_nat_iso : homomorphism natural_isomorphism.
diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v
index faf4759bd..5e1d5d8c3 100644
--- a/theories/Numbers/Natural/Abstract/NMinus.v
+++ b/theories/Numbers/Natural/Abstract/NMinus.v
@@ -63,8 +63,8 @@ Proof.
 intros n m p; induct p.
 intro; now do 2 rewrite minus_0_r.
 intros p IH H. do 2 rewrite minus_succ_r.
-rewrite <- IH; [apply lt_le_incl; now apply -> le_succ_l |].
-rewrite plus_pred_r. apply minus_gt. now apply -> le_succ_l.
+rewrite <- IH by (apply lt_le_incl; now apply -> le_succ_l).
+rewrite plus_pred_r by (apply minus_gt; now apply -> le_succ_l).
 reflexivity.
 Qed.
 
@@ -76,13 +76,13 @@ Qed.
 
 Theorem plus_minus : forall n m : N, (n + m) - m == n.
 Proof.
-intros n m. rewrite <- plus_minus_assoc. apply le_refl.
+intros n m. rewrite <- plus_minus_assoc by (apply le_refl).
 rewrite minus_diag; now rewrite plus_0_r.
 Qed.
 
 Theorem minus_plus : forall n m : N, n <= m -> (m - n) + n == m.
 Proof.
-intros n m H. rewrite plus_comm. rewrite plus_minus_assoc; [assumption |].
+intros n m H. rewrite plus_comm. rewrite plus_minus_assoc by assumption.
 rewrite plus_comm. apply plus_minus.
 Qed.
 
@@ -121,7 +121,7 @@ Theorem plus_minus_swap : forall n m p : N, p <= n -> n + m - p == n - p + m.
 Proof.
 intros n m p H.
 rewrite (plus_comm n m).
-rewrite <- plus_minus_assoc; [assumption |].
+rewrite <- plus_minus_assoc by assumption.
 now rewrite (plus_comm m (n - p)).
 Qed.
 
@@ -151,8 +151,8 @@ Proof.
 intros n m; cases m.
 now rewrite pred_0, times_0_r, minus_0_l.
 intro m; rewrite pred_succ, times_succ_r, <- plus_minus_assoc.
-now apply eq_le_incl.
 now rewrite minus_diag, plus_0_r.
+now apply eq_le_incl.
 Qed.
 
 Theorem times_minus_distr_r : forall n m p : N, (n - m) * p == n * p - m * p.
@@ -160,9 +160,9 @@ Proof.
 intros n m p; induct n.
 now rewrite minus_0_l, times_0_l, minus_0_l.
 intros n IH. destruct (le_gt_cases m n) as [H | H].
-rewrite minus_succ_l; [assumption |]. do 2 rewrite times_succ_l.
+rewrite minus_succ_l by assumption. do 2 rewrite times_succ_l.
 rewrite (plus_comm ((n - m) * p) p), (plus_comm (n * p) p).
-rewrite <- (plus_minus_assoc p (n * p) (m * p)); [now apply times_le_mono_r |].
+rewrite <- (plus_minus_assoc p (n * p) (m * p)) by now apply times_le_mono_r.
 now apply <- plus_cancel_l.
 assert (H1 : S n <= m); [now apply <- le_succ_l |].
 setoid_replace (S n - m) with 0 by now apply <- minus_0_le.
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index 7b4645be3..1e53d8063 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -506,7 +506,7 @@ Theorem pred_lt_mono : forall n m : N, n ~= 0 -> (n < m <-> P n < P m).
 Proof.
 intros n m H1; split; intro H2.
 assert (m ~= 0). apply <- neq_0_lt_0. now apply lt_lt_0 with n.
-now rewrite <- (succ_pred n) in H2; rewrite <- (succ_pred m) in H2;
+now rewrite <- (succ_pred n) in H2; rewrite <- (succ_pred m) in H2 ;
 [apply <- succ_lt_mono | | |].
 assert (m ~= 0). apply <- neq_0_lt_0. apply lt_lt_0 with (P n).
 apply lt_le_trans with (P m). assumption. apply le_pred_l.
@@ -515,7 +515,7 @@ Qed.
 
 Theorem lt_succ_lt_pred : forall n m : N, S n < m <-> n < P m.
 Proof.
-intros n m. rewrite pred_lt_mono. apply neq_succ_0. now rewrite pred_succ.
+intros n m. rewrite pred_lt_mono by apply neq_succ_0. now rewrite pred_succ.
 Qed.
 
 Theorem le_succ_le_pred : forall n m : N, S n <= m -> n <= P m. (* Converse is false for n == m == 0 *)
diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v
index 78034802f..8672592d9 100644
--- a/theories/QArith/Qpower.v
+++ b/theories/QArith/Qpower.v
@@ -121,8 +121,8 @@ destruct (Qeq_dec a 0).
  rewrite q.
  repeat rewrite Qpower_positive_0.
  reflexivity.
-rewrite <- (Qdiv_mult_l (Qpower_positive a (n - m)) (Qpower_positive a m)).
- apply Qpower_not_0_positive; assumption.
+rewrite <- (Qdiv_mult_l (Qpower_positive a (n - m)) (Qpower_positive a m)) by
+ (apply Qpower_not_0_positive; assumption).
 apply Qdiv_comp;[|reflexivity].
 rewrite Qmult_comm.
 rewrite <- Qpower_plus_positive.
@@ -150,8 +150,7 @@ Proof.
 intros a n m H.
 destruct (Qeq_dec a 0)as [X|X].
 rewrite X.
-rewrite Qpower_0.
-assumption.
+rewrite Qpower_0 by assumption.
 destruct n; destruct m; try (elim H; reflexivity);
  simpl; repeat rewrite Qpower_positive_0; ring_simplify;
  reflexivity.
@@ -191,9 +190,8 @@ induction n using Pind.
 rewrite Zpos_succ_morphism.
 unfold Zsucc.
 rewrite Zpower_exp; auto with *; try discriminate.
-rewrite Qpower_plus'; try discriminate.
-rewrite <- IHn.
- discriminate.
+rewrite Qpower_plus' by discriminate.
+rewrite <- IHn by discriminate.
 replace (a^'n*a^1)%Z with (a^'n*a)%Z by ring.
 ring_simplify.
 reflexivity.