unification encore...

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

3 files changed, 2 insertions, 36 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 27ae5ebd9..bc50fdd2a 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -31,13 +31,6 @@ open Tacexpr
 open Clenv
 
     
-let clenv_wtactic wt clenv =
-  { templval = clenv.templval;
-    templtyp = clenv.templtyp;
-    namenv = clenv.namenv;
-    env = clenv.env;
-    hook = wt clenv.hook }
-
 (* This function put casts around metavariables whose type could not be
  * infered by the refiner, that is head of applications, predicates and
  * subject of Cases.
@@ -94,27 +87,10 @@ let elim_res_pf_THEN_i clenv tac gls =
   let clenv' = (clenv_unique_resolver true clenv gls) in
   tclTHENLASTn (clenv_refine clenv') (tac clenv') gls
 
-(* [clenv_pose_dependent_evars clenv]
- * For each dependent evar in the clause-env which does not have a value,
- * pose a value for it by constructing a fresh evar.  We do this in
- * left-to-right order, so that every evar's type is always closed w.r.t.
- * metas. *)
-
-let clenv_pose_dependent_evars clenv =
-  let dep_mvs = clenv_dependent false clenv in
-  List.fold_left
-    (fun clenv mv ->
-       let evar = Evarutil.new_evar_in_sign (get_env clenv.hook) in
-       let (evar_n,_) = destEvar evar in
-       let tY = clenv_instance_type clenv mv in
-       let clenv' = clenv_wtactic (w_Declare evar_n tY) clenv in
-       clenv_assign mv evar clenv')
-    clenv
-    dep_mvs
 
 let e_res_pf clenv gls =
-  clenv_refine
-    (clenv_pose_dependent_evars (clenv_unique_resolver false clenv gls)) gls
+  clenv_refine (evar_clenv_unique_resolver clenv gls) gls
+
 
 
 
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 2e2060349..41b910222 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -43,12 +43,6 @@ let extract_decl sp evc =
 let restore_decl sp evd evc =
   (rc_add evc (sp,evd))
 
-let w_Declare sp ty (wc : named_context sigma) =
-  let _ = Typing.type_of (get_env wc) wc.sigma ty in (* Utile ?? *)
-  let sign = get_hyps wc in
-  let newdecl = mk_goal sign ty in 
-  ((rc_add wc (sp,newdecl)): named_context sigma)
-
 (******************************************)
 (* Instantiation of existential variables *)
 (******************************************)
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 54646caf8..4766d94cb 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -22,15 +22,11 @@ type wc = named_context sigma (* for a better reading of the following *)
 
 (* Refinement of existential variables. *)
 
-val rc_of_glsigma : goal sigma -> wc
-
 (* A [w_tactic] is a tactic which modifies the a set of evars of which
    a goal depend, either by instantiating one, or by declaring a new
    dependent goal *)
 type w_tactic = wc -> wc
 
-val w_Declare    : evar -> types -> w_tactic
-
 val w_refine :  evar -> Rawterm.rawconstr  -> w_tactic
 
 val instantiate_pf_com :