Start documenting new [rewrite_strat] tactic that applies rewriting

according to a given strategy.
- Enhance the hints/lemmas strategy to support "using tac" comming from
rewrite hints to solve side-conditions.  


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

9 files changed, 217 insertions, 64 deletions

diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
index c0913135c..8a293ea2b 100644
--- a/doc/refman/Setoid.tex
+++ b/doc/refman/Setoid.tex
@@ -1,15 +1,16 @@
 \newtheorem{cscexample}{Example}
 
-\achapter{\protect{User defined equalities and relations}}
+\achapter{\protect{Generalized rewriting}}
 \aauthor{Matthieu Sozeau}
-\tacindex{setoid\_replace}
 \label{setoid_replace}
 
-This chapter presents the extension of several equality related tactics to
-work over user-defined structures (called setoids) that are equipped with
-ad-hoc equivalence relations meant to behave as equalities.
-Actually, the tactics have also been generalized to relations weaker then
-equivalences (e.g. rewriting systems).
+This chapter presents the extension of several equality related tactics
+to work over user-defined structures (called setoids) that are equipped
+with ad-hoc equivalence relations meant to behave as equalities.
+Actually, the tactics have also been generalized to relations weaker
+then equivalences (e.g. rewriting systems). The toolbox also extends the
+automatic rewriting capabilities of the system, allowing to specify
+custom strategies for rewriting.
 
 This documentation is adapted from the previous setoid documentation by
 Claudio Sacerdoti Coen (based on previous work by Cl\'ement Renard).
@@ -43,7 +44,9 @@ the previous implementation in several ways:
   user to customize the proof-search if necessary.
 \end{itemize}
 
-\asection{Relations and morphisms}
+\asection{Introduction to generalized rewriting}
+
+\subsection{Relations and morphisms}
 
 A parametric \emph{relation} \texttt{R} is any term of type
 \texttt{forall ($x_1$:$T_1$) \ldots ($x_n$:$T_n$), relation $A$}. The
@@ -162,7 +165,7 @@ will fail replacing the third occurrence of \texttt{S2} unless \texttt{f}
 has also been declared as a morphism.
 \end{cscexample}
 
-\asection{Adding new relations and morphisms}
+\subsection{Adding new relations and morphisms}
 A parametric relation
 \textit{Aeq}\texttt{: forall ($y_1 : \beta_!$ \ldots $y_m : \beta_m$), relation (A $t_1$ \ldots $t_n$)} over
 \textit{(A : $\alpha_i$ -> \ldots $\alpha_n$ -> }\texttt{Type})
@@ -329,7 +332,7 @@ declaration (see \S\ref{setoid:first-class}) at definition time.
 When loading a compiled file or importing a module,
 all the declarations of this module will be loaded.
 
-\asection{Rewriting and non reflexive relations}
+\subsection{Rewriting and non reflexive relations}
 To replace only one argument of an n-ary morphism it is necessary to prove
 that all the other arguments are related to themselves by the respective
 relation instances.
@@ -360,7 +363,7 @@ non zero elements). Division can be declared as a morphism of signature
 is equivalent to \texttt{n=n $\land$ n$\neq$0}.
 \end{cscexample}
 
-\asection{Rewriting and non symmetric relations}
+\subsection{Rewriting and non symmetric relations}
 When the user works up to relations that are not symmetric, it is no longer
 the case that any covariant morphism argument is also contravariant. As a
 result it is no longer possible to replace a term with a related one in
@@ -408,7 +411,7 @@ is contravariant in its second argument), and finally covariantly in
 is contravariant in its first argument with respect to the relation itself).
 \end{cscexample}
 
-\asection{Rewriting in ambiguous setoid contexts}
+\subsection{Rewriting in ambiguous setoid contexts}
 One function can respect several different relations and thus it can be
 declared as a morphism having multiple signatures.
 
@@ -431,7 +434,8 @@ tactic will always choose the first possible solution to the set of
 constraints generated by a rewrite and will not try to find \emph{all}
 possible solutions to warn the user about.
 
-\asection{First class setoids and morphisms}
+\asection{Commands and tactics}
+\subsection{First class setoids and morphisms}
 \label{setoid:first-class}
 
 The implementation is based on a first-class representation of
@@ -507,7 +511,7 @@ Proof. intros. rewrite H. reflexivity. Qed.
 \end{coq_example*}
 \end{cscexample}
 
-\asection{Tactics enabled on user provided relations}
+\subsection{Tactics enabled on user provided relations}
 \label{setoidtactics}
 The following tactics, all prefixed by \texttt{setoid\_}, 
 deal with arbitrary
@@ -519,20 +523,20 @@ the prefixed tactics it is possible to pass additional arguments such as
 \texttt{using relation}.
 \medskip
 
-\comindex{setoid\_reflexivity}
+\tacindex{setoid\_reflexivity}
 \texttt{setoid\_reflexivity}
 
-\comindex{setoid\_symmetry}
+\tacindex{setoid\_symmetry}
 \texttt{setoid\_symmetry} \zeroone{\texttt{in} \textit{ident}}
 
-\comindex{setoid\_transitivity}
+\tacindex{setoid\_transitivity}
 \texttt{setoid\_transitivity}
 
-\comindex{setoid\_rewrite}
+\tacindex{setoid\_rewrite}
 \texttt{setoid\_rewrite} \zeroone{\textit{orientation}} \textit{term}
 ~\zeroone{\texttt{at} \textit{occs}} ~\zeroone{\texttt{in} \textit{ident}}
 
-\comindex{setoid\_replace}
+\tacindex{setoid\_replace}
 \texttt{setoid\_replace} \textit{term} \texttt{with} \textit{term}
 ~\zeroone{\texttt{in} \textit{ident}}
 ~\zeroone{\texttt{using relation} \textit{term}}
@@ -557,7 +561,7 @@ not proof of Leibniz equalities. In particular it is possible to exploit
 \texttt{autorewrite} to simulate normalization in a term rewriting system
 up to user defined equalities.
 
-\asection{Printing relations and morphisms}
+\subsection{Printing relations and morphisms}
 The \texttt{Print Instances} command can be used to show the list of
 currently registered \texttt{Reflexive} (using \texttt{Print Instances Reflexive}),
 \texttt{Symmetric} or \texttt{Transitive} relations,
@@ -568,7 +572,7 @@ because the latter is not a composition of morphisms, the \texttt{Print Instance
 commands can be useful to understand what additional morphisms should be
 registered.
 
-\asection{Deprecated syntax and backward incompatibilities}
+\subsection{Deprecated syntax and backward incompatibilities}
 Due to backward compatibility reasons, the following syntax for the
 declaration of setoids and morphisms is also accepted.
 
@@ -607,7 +611,8 @@ contexts that were refused by the old implementation. As discussed in
 the next section, the semantics of the new \texttt{setoid\_rewrite}
 command differs slightly from the old one and \texttt{rewrite}.
 
-\asection{Rewriting under binders}
+\asection{Extensions}
+\subsection{Rewriting under binders}
 
 \textbf{Warning}: Due to compatibility issues, this feature is enabled only when calling 
 the \texttt{setoid\_rewrite} tactics directly and not \texttt{rewrite}.
@@ -678,7 +683,7 @@ and in its local environment, and all matches are rewritten
 \texttt{setoid\_rewrite} implementation can almost be recovered using
 the \texttt{at 1} modifier.
 
-\asection{Sub-relations}
+\subsection{Sub-relations}
 
 Sub-relations can be used to specify that one relation is included in
 another, so that morphisms signatures for one can be used for the other.
@@ -698,14 +703,136 @@ any rewriting constraints arising from a rewrite using \texttt{iff},
 Sub-relations are implemented in \texttt{Classes.Morphisms} and are a 
 prime example of a mostly user-space extension of the algorithm.
 
-\asection{Constant unfolding}
+\subsection{Constant unfolding}
 
 The resolution tactic is based on type classes and hence regards user-defined 
 constants as transparent by default. This may slow down the resolution
 due to a lot of unifications (all the declared \texttt{Proper}
 instances are tried at each node of the search tree).
 To speed it up, declare your constant as rigid for proof search
-using the command \texttt{Typeclasses Opaque} (see \S \ref{TypeclassesTransparency}).
+using the command \texttt{Typeclasses Opaque} (see \S
+\ref{TypeclassesTransparency}).
+
+\asection{Strategies for rewriting}
+
+\subsection{Definitions}
+The generalized rewriting tactic is based on a set of strategies that
+can be combined to obtain custom rewriting procedures. Its set of
+strategies is based on Elan's rewriting strategies
+\cite{Luttik97specificationof}. Rewriting strategies are applied using
+the tactic $\texttt{rewrite\_strat}~s$ where $s$ is a strategy
+expression. Strategies are defined inductively as described by the
+following grammar:
+
+\def\str#1{\texttt{#1}}
+
+\def\strline#1#2{& \vert & #1 & \text{#2}}
+\def\strlinea#1#2#3{& \vert & \str{#1}~#2 & \text{#3}}
+
+\[\begin{array}{lcll}
+  s, t, u & ::= & ( s ) & \text{strategy} \\
+  \strline{c}{lemma} \\
+  \strline{\str{<-}~c}{lemma, right-to-left} \\
+
+  \strline{\str{fail}}{failure} \\
+  \strline{\str{id}}{identity} \\
+  \strline{\str{refl}}{reflexivity} \\
+  \strlinea{progress}{s}{progress} \\
+  \strlinea{try}{s}{failure catch} \\
+
+  \strline{s~\str{;}~u}{composition} \\
+  \strline{\str{choice}~s~t}{left-biased choice} \\
+
+  \strlinea{repeat}{s}{iteration (+)} \\
+  \strlinea{any}{s}{iteration (*)} \\
+  
+  \strlinea{subterm}{s}{one subterm} \\
+  \strlinea{subterms}{s}{all subterms} \\
+  \strlinea{innermost}{s}{innermost first} \\
+  \strlinea{outermost}{s}{outermost first}\\
+  \strlinea{bottomup}{s}{bottom-up} \\
+  \strlinea{topdown}{s}{top-down} \\
+
+  \strlinea{hints}{hintdb}{apply hint} \\
+  \strlinea{terms}{c \ldots c}{any of the terms}\\
+  \strlinea{eval}{redexpr}{apply reduction}\\
+  \strlinea{fold}{c}{fold expression}
+\end{array}\]
+
+Actually a few of these are defined in term of the others using
+a primitive fixpoint operator:
+
+\[\begin{array}{lcl}
+  \str{try}~s & = & \str{choice}~s~\str{id} \\
+  \str{any}~s & = & \str{fix}~u. \str{try}~(s~\str{;}~u) \\
+  \str{repeat}~s & = & s~\str{;}~\str{any}~s \\
+  \str{bottomup}~s & = &
+  \str{fix}~bu. (\str{choice}~(\str{progress}~(\str{subterms}~bu))~s)~\str{;}~\str{try}~bu \\
+  \str{topdown}~s & = &
+  \str{fix}~td. (\str{choice}~s~(\str{progress}~(\str{subterms}~td)))~\str{;}~\str{try}~td \\
+  \str{innermost}~s & = &  \str{fix}~i. (\str{choice}~(\str{subterm}~i)~s) \\
+  \str{outermost}~s & = &
+  \str{fix}~o. (\str{choice}~s~(\str{subterm}~o))
+\end{array}\]
+
+The basic control strategy semantics are straightforward: strategies are
+applied to subterms of the term to rewrite, starting from the root of
+the term. The lemma strategies unify the left-hand-side of the
+lemma with the current subterm and on success rewrite it to the
+right-hand-side. Composition can be used to continue rewriting on the
+current subterm. The fail strategy always fails while the identity
+strategy succeeds without making progress. The reflexivity strategy
+succeeds, making progress using a reflexivity proof of
+rewriting. Progress tests progress of the argument strategy and fails if
+no progress was made, while \str{try} always succeeds, catching
+failures. Choice is left-biased: it will launch the first strategy and
+fall back on the second one in case of failure. One can iterate a
+strategy at least 1 time using \str{repeat} and at least 0 times using
+\str{any}.
+
+The \str{subterm} and \str{subterms} strategies apply their argument
+strategy $s$ to respectively one or all subterms of the current term
+under consideration, left-to-right. \str{subterm} stops at the first
+subterm for which $s$ made progress. The composite strategies
+\str{innermost} and \str{outermost} perform a single innermost our outermost
+rewrite using their argument strategy. Their counterparts
+\str{bottomup} and \str{topdown} perform as many rewritings as possible,
+starting from the bottom or the top of the term. 
+
+Hint databases created for \texttt{autorewrite} can also be used by
+\texttt{rewrite\_strat} using the \str{hints} strategy that applies any
+of the lemmas at the current subterm. The \str{terms} strategy takes the
+lemma names directly as arguments. The \str{eval} strategy expects a
+reduction expression (see \S\ref{Conversion-tactics}) and succeeds if it
+reduces the subterm under consideration. The \str{fold} strategy takes a
+term $c$ and tries to \emph{unify} it to the current subterm, converting
+it to $c$ on success, it is stronger than the tactic \texttt{fold}. 
+
+
+\subsection{Usage}
+\tacindex{rewrite\_strat}
+
+\texttt{rewrite\_strat}~\textit{s}~\zeroone{\texttt{in} \textit{ident}}: 
+
+  Rewrite using the strategy \textit{s} in hypothesis \textit{ident}
+  or the conclusion.
+
+  \begin{ErrMsgs}
+  \item  \errindex{Nothing to rewrite}. If the strategy failed. 
+  \item  \errindex{No progress made}. If the strategy succeeded but
+    made no progress.
+  \item  \errindex{Unable to satisfy the rewriting constraints}. 
+    If the strategy succeeded and made progress but the corresponding
+    rewriting constraints are not satisfied.
+  \end{ErrMsgs}
+  
+
+The \texttt{setoid\_rewrite}~c tactic is basically equivalent to 
+\texttt{rewrite\_strat}~(\str{outermost}~c).
+
+
+
+
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
index 192a96998..3715c4c79 100644
--- a/doc/refman/biblio.bib
+++ b/doc/refman/biblio.bib
@@ -786,6 +786,13 @@ of the {ML} language},
   year        = {1990}
 }
 
+@inproceedings{Luttik97specificationof,
+	Author = {Sebastiaan P. Luttik and Eelco Visser},
+	Booktitle = {2nd International Workshop on the Theory and Practice of Algebraic Specifications (ASF+SDF'97), Electronic Workshops in Computing},
+	Publisher = {Springer-Verlag},
+	Title = {Specification of Rewriting Strategies},
+	Year = {1997}}
+
 @Book{MaL84,
   author      = {{P. Martin-L\"of}},
   publisher   = {Bibliopolis},
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index bc6da8c34..3f3b40bed 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -308,19 +308,19 @@ let clenv_unique_resolver ?(flags=default_unify_flags) clenv gl =
 *)
 
 let clenv_pose_metas_as_evars clenv dep_mvs =
-  let rec fold clenv = function
-  | [] -> clenv
+  let rec fold clenv l = function
+  | [] -> clenv, l
   | mv::mvs ->
       let ty = clenv_meta_type clenv mv in
       (* Postpone the evar-ization if dependent on another meta *)
       (* This assumes no cycle in the dependencies - is it correct ? *)
-      if occur_meta ty then fold clenv (mvs@[mv])
+      if occur_meta ty then fold clenv l (mvs@[mv])
       else
 	let (evd,evar) =
 	  new_evar clenv.evd (cl_env clenv) ~src:(Loc.ghost,Evar_kinds.GoalEvar) ty in
 	let clenv = clenv_assign mv evar {clenv with evd=evd} in
-	fold clenv mvs in
-  fold clenv dep_mvs
+	fold clenv (destEvar evar::l) mvs in
+  fold clenv [] dep_mvs
 
 let evar_clenv_unique_resolver = clenv_unique_resolver
 
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index bfb5ee27c..f80bff396 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -73,7 +73,7 @@ val evar_clenv_unique_resolver :
 
 val clenv_dependent : clausenv -> metavariable list
 
-val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv
+val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv * existential list
 
 (** {6 Bindings } *)
 
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 389075c9a..23a835ede 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -55,7 +55,7 @@ let clenv_pose_dependent_evars with_evars clenv =
   if not (List.is_empty dep_mvs) && not with_evars then
     raise
       (RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs)));
-  clenv_pose_metas_as_evars clenv dep_mvs
+  fst (clenv_pose_metas_as_evars clenv dep_mvs)
 
 let clenv_refine with_evars ?(with_classes=true) clenv gls =
   let clenv = clenv_pose_dependent_evars with_evars clenv in
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 39e0c653c..4ebe089e9 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -25,13 +25,13 @@ type rew_rule = { rew_lemma: constr;
 		  rew_type: types;
 		  rew_pat: constr;
 		  rew_l2r: bool;
-		  rew_tac: glob_tactic_expr }
+		  rew_tac: glob_tactic_expr option }
 
 let subst_hint subst hint =
   let cst' = subst_mps subst hint.rew_lemma in
   let typ' = subst_mps subst hint.rew_type in
   let pat' = subst_mps subst hint.rew_pat in
-  let t' = Tacsubst.subst_tactic subst hint.rew_tac in
+  let t' = Option.smartmap (Tacsubst.subst_tactic subst) hint.rew_tac in
     if hint.rew_lemma == cst' && hint.rew_type == typ' && hint.rew_tac == t' then hint else
       { hint with
 	rew_lemma = cst'; rew_type = typ';
@@ -82,16 +82,18 @@ let print_rewrite_hintdb bas =
 	   (fun h ->
 	     str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++
 	       Printer.pr_lconstr h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr h.rew_type ++
-	       str " then use tactic " ++
-	       Pptactic.pr_glob_tactic (Global.env()) h.rew_tac)
+	       Option.cata (fun tac -> str " then use tactic " ++
+	       Pptactic.pr_glob_tactic (Global.env()) tac) (mt ()) h.rew_tac)
 	   (find_rewrites bas))
 
-type raw_rew_rule = Loc.t * constr * bool * raw_tactic_expr
+type raw_rew_rule = Loc.t * constr * bool * raw_tactic_expr option
 
 (* Applies all the rules of one base *)
 let one_base general_rewrite_maybe_in tac_main bas =
   let lrul = find_rewrites bas in
-  let lrul = List.map (fun h -> (h.rew_lemma,h.rew_l2r,Tacinterp.eval_tactic h.rew_tac)) lrul in
+  let lrul = List.map (fun h -> 
+  let tac = match h.rew_tac with None -> tclIDTAC | Some t -> Tacinterp.eval_tactic t in
+    (h.rew_lemma,h.rew_l2r,tac)) lrul in
     tclREPEAT_MAIN (tclPROGRESS (List.fold_left (fun tac (csr,dir,tc) ->
       tclTHEN tac
         (tclREPEAT_MAIN
@@ -104,7 +106,7 @@ let autorewrite ?(conds=Naive) tac_main lbas =
     (List.fold_left (fun tac bas ->
        tclTHEN tac
         (one_base (fun dir c tac ->
-	  let tac = tac, conds in
+	  let tac = (tac, conds) in
 	    general_rewrite dir AllOccurrences true false ~tac c)
 	  tac_main bas))
       tclIDTAC lbas))
@@ -238,7 +240,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
     let eqclause = Clenv.mk_clenv_from_env env sigma None (c,ty) in
     let eqclause =
       if metas then eqclause
-      else clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd)
+      else fst (clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd))
     in
     let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
     let rec split_last_two = function
@@ -286,7 +288,7 @@ let add_rew_rules base lrul =
 	let pat = if b then info.hyp_left else info.hyp_right in
 	let rul = { rew_lemma = c; rew_type = info.hyp_ty;
 		    rew_pat = pat; rew_l2r = b;
-		    rew_tac = Tacintern.glob_tactic t}
+		    rew_tac = Option.map Tacintern.glob_tactic t}
 	in incr counter;
 	  HintDN.add pat (!counter, rul) dn) HintDN.empty lrul
   in Lib.add_anonymous_leaf (inHintRewrite (base,lrul))
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index 773e3694e..9ddabc584 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -12,7 +12,7 @@ open Tacmach
 open Equality
 
 (** Rewriting rules before tactic interpretation *)
-type raw_rew_rule = Loc.t * Term.constr * bool * Tacexpr.raw_tactic_expr
+type raw_rew_rule = Loc.t * Term.constr * bool * Tacexpr.raw_tactic_expr option
 
 (** To add rewriting rules to a base *)
 val add_rew_rules : string -> raw_rew_rule list -> unit
@@ -29,7 +29,7 @@ type rew_rule = { rew_lemma: constr;
 		  rew_type: types;
 		  rew_pat: constr;
 		  rew_l2r: bool;
-		  rew_tac: glob_tactic_expr }
+		  rew_tac: glob_tactic_expr option }
 
 val find_rewrites : string -> rew_rule list
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 75fedc598..e14c23421 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -259,14 +259,14 @@ let add_rewrite_hint bases ort t lcsr =
 
 VERNAC COMMAND EXTEND HintRewrite
   [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] ->
-  [ add_rewrite_hint bl o (Tacexpr.TacId []) l ]
+  [ add_rewrite_hint bl o None l ]
 | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
     ":" preident_list(bl) ] ->
-  [ add_rewrite_hint bl o t l ]
+  [ add_rewrite_hint bl o (Some t) l ]
 | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] ->
-  [ add_rewrite_hint ["core"] o (Tacexpr.TacId []) l ]
+  [ add_rewrite_hint ["core"] o None l ]
 | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] ->
-  [ add_rewrite_hint ["core"] o t l ]
+  [ add_rewrite_hint ["core"] o (Some t) l ]
 END
 
 (**********************************************************************)
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 0e6654545..f7c13d01a 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -348,7 +348,22 @@ let refresh_hypinfo env sigma hypinfo =
 	| _ -> hypinfo
   else hypinfo
 
-let unify_eqn env sigma hypinfo t =
+
+let solve_remaining_by by env prf =
+  match by with
+  | None -> env, prf
+  | Some tac ->
+    let indep = clenv_independent env in
+    let tac = eval_tactic tac in
+    let evd' = 
+      List.fold_right (fun mv evd ->
+        let ty = Clenv.clenv_nf_meta env (meta_type evd mv) in
+	let c = Pfedit.build_by_tactic env.env ty (tclCOMPLETE tac) in
+	  meta_assign mv (c, (Conv,TypeNotProcessed)) evd)
+      indep env.evd
+    in { env with evd = evd' }, prf
+
+let unify_eqn env sigma hypinfo by t =
   if isEvar t then None
   else try
     let {cl=cl; prf=prf; car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=c; abs=abs} = !hypinfo in
@@ -365,10 +380,11 @@ let unify_eqn env sigma hypinfo t =
 (* 	  let env' = Clenv.clenv_pose_metas_as_evars env' (Evd.undefined_metas env'.evd) in *)
 	  let evd' = Typeclasses.resolve_typeclasses ~fail:true env'.env env'.evd in
 	  let env' = { env' with evd = evd' } in
-	  let nf c = Evarutil.nf_evar evd' (Clenv.clenv_nf_meta env' c) in
+	  let env', prf = solve_remaining_by by env' (Clenv.clenv_value env') in	   
+	  let nf c = Evarutil.nf_evar env'.evd (Clenv.clenv_nf_meta env' c) in
 	  let c1 = nf c1 and c2 = nf c2
 	  and car = nf car and rel = nf rel
-	  and prf = nf (Clenv.clenv_value env') in
+	  and prf = nf prf in
 	  let ty1 = Typing.type_of env'.env env'.evd c1
 	  and ty2 = Typing.type_of env'.env env'.evd c2
 	  in
@@ -633,7 +649,7 @@ let apply_constraint env avoid car rel prf cstr res =
 
 let eq_env x y = x == y
 
-let apply_rule hypinfo loccs : strategy =
+let apply_rule hypinfo by loccs : strategy =
   let (nowhere_except_in,occs) = convert_occs loccs in
   let is_occ occ =
     if nowhere_except_in then List.mem occ occs else not (List.mem occ occs) in
@@ -641,7 +657,7 @@ let apply_rule hypinfo loccs : strategy =
     fun env avoid t ty cstr evars ->
       if not (eq_env !hypinfo.cl.env env) then
 	hypinfo := refresh_hypinfo env (goalevars evars) !hypinfo;
-      let unif = unify_eqn env (goalevars evars) hypinfo t in
+      let unif = unify_eqn env (goalevars evars) hypinfo by t in
 	if not (Option.is_empty unif) then incr occ;
 	match unif with
 	| Some (evd', (prf, (car, rel, c1, c2))) when is_occ !occ ->
@@ -655,10 +671,10 @@ let apply_rule hypinfo loccs : strategy =
 	    end
 	| _ -> None
 
-let apply_lemma flags (evm,c) left2right loccs : strategy =
+let apply_lemma flags (evm,c) left2right by loccs : strategy =
   fun env avoid t ty cstr evars ->
     let hypinfo = ref (decompose_applied_relation env (goalevars evars) flags None c left2right) in
-      apply_rule hypinfo loccs env avoid t ty cstr evars
+      apply_rule hypinfo by loccs env avoid t ty cstr evars
 
 let make_leibniz_proof c ty r =
   let prf = 
@@ -1010,8 +1026,8 @@ module Strategies =
       fix (fun out -> choice s (one_subterm out))
 
     let lemmas flags cs : strategy =
-      List.fold_left (fun tac (l,l2r) ->
-	choice tac (apply_lemma flags l l2r AllOccurrences))
+      List.fold_left (fun tac (l,l2r,by) ->
+	choice tac (apply_lemma flags l l2r by AllOccurrences))
 	fail cs
 
     let inj_open c = (Evd.empty,c)
@@ -1019,12 +1035,13 @@ module Strategies =
     let old_hints (db : string) : strategy =
       let rules = Autorewrite.find_rewrites db in
 	lemmas rewrite_unif_flags
-	  (List.map (fun hint -> (inj_open (hint.Autorewrite.rew_lemma, NoBindings), hint.Autorewrite.rew_l2r)) rules)
+	  (List.map (fun hint -> (inj_open (hint.Autorewrite.rew_lemma, NoBindings), hint.Autorewrite.rew_l2r, hint.Autorewrite.rew_tac)) rules)
 
     let hints (db : string) : strategy =
       fun env avoid t ty cstr evars ->
       let rules = Autorewrite.find_matches db t in
-      let lemma hint = (inj_open (hint.Autorewrite.rew_lemma, NoBindings), hint.Autorewrite.rew_l2r) in
+      let lemma hint = (inj_open (hint.Autorewrite.rew_lemma, NoBindings), hint.Autorewrite.rew_l2r,
+			hint.Autorewrite.rew_tac) in
       let lems = List.map lemma rules in
 	lemmas rewrite_unif_flags lems env avoid t ty cstr evars
 
@@ -1078,7 +1095,7 @@ end
 (** The strategy for a single rewrite, dealing with occurences. *)
 
 let rewrite_strat flags occs hyp =
-  let app = apply_rule hyp occs in
+  let app = apply_rule hyp None occs in
   let rec aux () =
     Strategies.choice app (subterm true flags (fun env -> aux () env))
   in aux ()
@@ -1359,22 +1376,22 @@ let occurrences_of = function
 let apply_constr_expr c l2r occs = fun env avoid t ty cstr evars ->
   let evd, c = Constrintern.interp_open_constr (goalevars evars) env c in
     apply_lemma (general_rewrite_unif_flags ()) (evd, (c, NoBindings)) 
-      l2r occs env avoid t ty cstr (evd, cstrevars evars)
+      l2r None occs env avoid t ty cstr (evd, cstrevars evars)
 
 let apply_glob_constr c l2r occs = fun env avoid t ty cstr evars ->
   let evd, c = (Pretyping.understand_tcc (goalevars evars) env c) in
     apply_lemma (general_rewrite_unif_flags ()) (evd, (c, NoBindings)) 
-      l2r occs env avoid t ty cstr (evd, cstrevars evars)
+      l2r None occs env avoid t ty cstr (evd, cstrevars evars)
 
 let interp_constr_list env sigma =
   List.map (fun c -> 
 	      let evd, c = Constrintern.interp_open_constr sigma env c in
-		(evd, (c, NoBindings)), true)
+		(evd, (c, NoBindings)), true, None)
 
 let interp_glob_constr_list env sigma =
   List.map (fun c -> 
 	      let evd, c = Pretyping.understand_tcc sigma env c in
-		(evd, (c, NoBindings)), true)
+		(evd, (c, NoBindings)), true, None)
 
 (* Syntax for rewriting with strategies *)
 
@@ -1945,7 +1962,7 @@ let general_rewrite_flags = { under_lambdas = false; on_morphisms = true }
 let apply_lemma gl (c,l) cl l2r occs =
   let sigma = project gl in
   let hypinfo = ref (get_hyp gl sigma (c,l) cl l2r) in
-  let app = apply_rule hypinfo occs in
+  let app = apply_rule hypinfo None occs in
   let rec aux () =
     Strategies.choice app (subterm true general_rewrite_flags (fun env -> aux () env))
   in !hypinfo, aux ()