Backtrack on unneeded change of interface for pose_metas_as_evars.

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

4 files changed, 8 insertions, 8 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 3f3b40bed..bc6da8c34 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 l = function
-  | [] -> clenv, l
+  let rec fold clenv = function
+  | [] -> clenv
   | 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 l (mvs@[mv])
+      if occur_meta ty then fold clenv (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 (destEvar evar::l) mvs in
-  fold clenv [] dep_mvs
+	fold clenv 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 f80bff396..bfb5ee27c 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 * existential list
+val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv
 
 (** {6 Bindings } *)
 
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 23a835ede..389075c9a 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)));
-  fst (clenv_pose_metas_as_evars clenv dep_mvs)
+  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 4ebe089e9..a4269b17c 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -240,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 fst (clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd))
+      else 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