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

3 files changed, 7 insertions, 7 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index bc6da8c347..3f3b40bedb 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 bfb5ee27ca..f80bff3965 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 389075c9ae..23a835edee 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