rewrite_db : a first attempt at using rewrite_strat for a quicker autorewrite

 rewrite_db fails if nothing has been rewritten, and it only performs
 *one* top-down pass. For the moment, use (repeat rewrite_db) for
 emulating more closely autorewrite.

 Btw, let's make Himsg.explain_ltac_call_trace robust wrt TacExtend
 with fun(ny) parts

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

4 files changed, 21 insertions, 7 deletions

diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v
index c172157f1c..e1424bb10e 100644
--- a/plugins/micromega/EnvRing.v
+++ b/plugins/micromega/EnvRing.v
@@ -617,7 +617,8 @@ Qed.
   (morph_opp CRmorph)
   : Esimpl.
 
- Ltac Esimpl := autorewrite with Esimpl; rsimpl; simpl.
+ (* Quicker than autorewrite with Esimpl :-) *)
+ Ltac Esimpl := try rewrite_db Esimpl; rsimpl; simpl.
 
  Lemma PaddC_ok c P l : (PaddC P c)@l == P@l + [c].
  Proof.
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index f6f7512683..4822a0c993 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -604,7 +604,8 @@ Section MakeRingPol.
   (morph_opp CRmorph)
   : Esimpl.
 
- Ltac Esimpl := autorewrite with Esimpl; rsimpl; simpl.
+ (* Quicker than autorewrite with Esimpl :-) *)
+ Ltac Esimpl := try rewrite_db Esimpl; rsimpl; simpl.
 
  Lemma PaddC_ok c P l : (PaddC P c)@l == P@l + [c].
  Proof.
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 2e7aed2b32..532f36c15e 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1528,9 +1528,16 @@ ARGUMENT EXTEND rewstrategy
   | [ "fold" constr(c) ] -> [ StratFold c ]
 END
 
+(* By default the strategy for "rewrite_db" is top-down *)
+
+let db_strat db = Strategies.td (Strategies.hints db)
+let cl_rewrite_clause_db db cl = cl_rewrite_clause_strat (db_strat db) cl
+
 TACTIC EXTEND rewrite_strat
 | [ "rewrite_strat" rewstrategy(s) "in" hyp(id) ] -> [ cl_rewrite_clause_strat s (Some id) ]
 | [ "rewrite_strat" rewstrategy(s) ] -> [ cl_rewrite_clause_strat s None ]
+| [ "rewrite_db" preident(db) "in" hyp(id) ] -> [ cl_rewrite_clause_db db (Some id) ]
+| [ "rewrite_db" preident(db) ] -> [ cl_rewrite_clause_db db None ]
 END
 
 let clsubstitute o c =
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index be8fbf89d1..0df2994b70 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -993,6 +993,11 @@ let explain_reduction_tactic_error = function
 let explain_ltac_call_trace (nrep,last,trace,loc) =
   let calls =
     (nrep,last) :: List.rev (List.map(fun(n,_,ck)->(n,ck))trace) in
+  let tacexpr_differ te te' =
+    (* NB: The following comparison may raise an exception
+       since a tacexpr may embed a functional part via a TacExtend *)
+    try te <> te' with Invalid_argument _ -> false
+  in
   let pr_call (n,ck) =
     (match ck with
        | Proof_type.LtacNotationCall s -> quote (str s)
@@ -1004,11 +1009,11 @@ let explain_ltac_call_trace (nrep,last,trace,loc) =
 	   (Pptactic.pr_glob_tactic (Global.env())
 	      (Tacexpr.TacAtom (Loc.ghost,te)))
 	   ++ (match !otac with
-		 | Some te' when (Obj.magic te' <> te) ->
-		     strbrk " (expanded to " ++ quote
-		       (Pptactic.pr_tactic (Global.env())
-			  (Tacexpr.TacAtom (Loc.ghost,te')))
-		     ++ str ")"
+		 | Some te' when tacexpr_differ (Obj.magic te') te ->
+		   strbrk " (expanded to " ++ quote
+		     (Pptactic.pr_tactic (Global.env())
+			(Tacexpr.TacAtom (Loc.ghost,te')))
+		   ++ str ")"
 		 | _ -> mt ())
        | Proof_type.LtacConstrInterp (c,(vars,unboundvars)) ->
 	   let filter =