hiding the meta_map in evar_defs

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

3 files changed, 18 insertions, 22 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index f9834f5229..8dcc8e06bb 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -567,7 +567,7 @@ let minimal_free_rels env sigma (c,cty) =
 
 let sig_clausal_form env sigma sort_of_ty siglen ty (dFLT,dFLTty) =
   let { intro = exist_term } = find_sigma_data sort_of_ty in 
-  let isevars = ref (Evarutil.create_evar_defs sigma) in
+  let isevars = ref (Evd.create_evar_defs sigma) in
   let rec sigrec_clausal_form siglen p_i =
     if siglen = 0 then
       if Evarconv.e_conv env isevars p_i dFLTty then
@@ -579,19 +579,18 @@ let sig_clausal_form env sigma sort_of_ty siglen ty (dFLT,dFLTty) =
       let (a,p_i_minus_1) = match whd_beta_stack p_i with
 	| (_sigS,[a;p]) -> (a,p)
  	| _ -> anomaly "sig_clausal_form: should be a sigma type" in
-      let ev = Evarutil.e_new_isevar isevars env (dummy_loc,InternalHole)
-	(Evarutil.new_Type ()) in
+      let ev = Evarutil.e_new_evar isevars env (new_Type ()) in
       let rty = beta_applist(p_i_minus_1,[ev]) in
       let tuple_tail = sigrec_clausal_form (siglen-1) rty in
       match
-	Evd.existential_opt_value (Evarutil.evars_of !isevars) 
+	Evd.existential_opt_value (Evd.evars_of !isevars) 
 	(destEvar ev)
       with
 	| Some w -> applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
 	| None -> anomaly "Not enough components to build the dependent tuple"
   in
   let scf = sigrec_clausal_form siglen ty in
-  Evarutil.nf_evar (Evarutil.evars_of !isevars) scf
+  Evarutil.nf_evar (Evd.evars_of !isevars) scf
 
 (* The problem is to build a destructor (a generalization of the
    predecessor) which, when applied to a term made of constructors
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index d65b1f3eb0..a0be2149a3 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -20,7 +20,7 @@ open Termops
 
 (* The instantiate tactic *)
 
-let evars_of evc c = 
+let evar_list evc c = 
   let rec evrec acc c =
     match kind_of_term c with
     | Evar (n, _) when Evd.in_dom evc n -> c :: acc
@@ -29,30 +29,30 @@ let evars_of evc c =
     evrec [] c
 
 let instantiate n rawc ido gl = 
-  let wc = Refiner.project_with_focus gl in
+  let sigma = gl.sigma in
   let evl = 
     match ido with
-	ConclLocation () -> evars_of wc.sigma gl.it.evar_concl 
+	ConclLocation () -> evar_list sigma gl.it.evar_concl 
       | HypLocation (id,hloc) ->
 	  let decl = lookup_named id gl.it.evar_hyps in
 	    match hloc with
 		InHyp ->  
 		  (match decl with 
-		       (_,None,typ) -> evars_of wc.sigma typ
+		       (_,None,typ) -> evar_list sigma typ
 		     | _ -> error 
 			 "please be more specific : in type or value ?")
 	      | InHypTypeOnly ->
-		  let (_, _, typ) = decl in evars_of wc.sigma typ
+		  let (_, _, typ) = decl in evar_list sigma typ
 	      | InHypValueOnly ->
 		  (match decl with 
-		       (_,Some body,_) -> evars_of wc.sigma body
+		       (_,Some body,_) -> evar_list sigma body
 		     | _ -> error "not a let .. in  hypothesis") in
     if List.length evl < n then
       error "not enough uninstantiated existential variables";
     if n <= 0 then error "incorrect existential variable index";
     let ev,_ =  destEvar (List.nth evl (n-1)) in
-    let wc' = w_refine ev rawc wc in
-      Tacticals.tclIDTAC {gl with sigma = wc'.sigma}
+    let evd' = w_refine (pf_env gl) ev rawc (create_evar_defs sigma)  in
+    Refiner.tclEVARS (evars_of evd') gl
 	
 (*
 let pfic gls c =
@@ -67,12 +67,9 @@ let instantiate_tac = function
   | _ -> invalid_arg "Instantiate called with bad arguments"
 *)
 
-let let_evar nam typ gls =
-  let sp = Evarutil.new_evar () in
-  let evd = Evarutil.create_evar_defs gls.sigma in
-  let evd' = Unification.w_Declare (pf_env gls) sp typ evd in
-  let ngls = {gls with sigma = Evarutil.evars_of evd'} in
-  let args = Array.of_list 
-	       (List.map mkVar (ids_of_named_context (pf_hyps gls))) in
-    Tactics.forward true nam (mkEvar(sp,args)) ngls
+let let_evar name typ gls =
+  let evd = Evd.create_evar_defs gls.sigma in
+  let evd',evar = Evarutil.new_evar evd (pf_env gls) typ in
+  Refiner.tclTHEN (Refiner.tclEVARS (evars_of evd'))
+    (Tactics.forward true name evar) gls
  
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 79aa71c0f4..3d91877d00 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -369,7 +369,7 @@ let general_elim_then_using
     match predicate with
        | None   -> elimclause'
        | Some p ->
-           clenv_unify true Reductionops.CONV (mkMeta pmv) p elimclause'
+           clenv_unify true Evd.CONV (mkMeta pmv) p elimclause'
   in 
   elim_res_pf_THEN_i elimclause' branchtacs gl