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

1 files changed, 14 insertions, 46 deletions

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 41b9102226..3033381431 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -8,40 +8,13 @@
 
 (* $Id$ *)
 
-open Pp
 open Util
 open Names
-open Rawterm
 open Term
-open Termops
-open Environ
 open Evd
 open Sign
-open Reductionops
-open Typing
-open Tacred
 open Proof_trees
-open Proof_type
-open Logic
 open Refiner
-open Tacexpr
-open Nameops
-
-
-type wc = named_context sigma (* for a better reading of the following *)
-
-let rc_of_glsigma sigma = rc_of_gc sigma.sigma sigma.it
-
-type w_tactic = named_context sigma -> named_context sigma
-
-let extract_decl sp evc =
-  let evdmap = evc.sigma in
-  let evd = Evd.map evdmap sp in 
-    { it = evd.evar_hyps;
-      sigma = Evd.rmv evdmap sp }
-
-let restore_decl sp evd evc =
-  (rc_add evc (sp,evd))
 
 (******************************************)
 (* Instantiation of existential variables *)
@@ -49,34 +22,29 @@ let restore_decl sp evd evc =
 
 (* w_tactic pour instantiate *) 
 
-let w_refine ev rawc wc =
-  if Evd.is_defined wc.sigma ev then 
+let w_refine env ev rawc evd =
+  if Evd.is_defined (evars_of evd) ev then 
     error "Instantiate called on already-defined evar";
-  let e_info = Evd.map wc.sigma ev in
-  let env = Evarutil.evar_env e_info in
-  let evd,typed_c = 
-    Pretyping.understand_gen_tcc wc.sigma env [] 
+  let e_info = Evd.map (evars_of evd) ev in
+  let env = Evd.evar_env e_info in
+  let sigma,typed_c = 
+    Pretyping.understand_gen_tcc (evars_of evd) env [] 
       (Some e_info.evar_concl) rawc in
   let inst_info = {e_info with evar_body = Evar_defined typed_c } in
-    restore_decl ev inst_info (extract_decl ev {wc with sigma=evd})
- (*   w_Define ev typed_c {wc with sigma=evd} *)
-
-(* the instantiate tactic was moved to tactics/evar_tactics.ml *) 
+  evar_define ev typed_c (evars_reset_evd sigma evd)
 
 (* vernac command Existential *)
 
 let instantiate_pf_com n com pfts = 
   let gls = top_goal_of_pftreestate pfts in
-  let wc = project_with_focus gls in
-  let sigma = wc.sigma in 
-  let (sp,evd) (* as evc *) = 
+  let sigma = gls.sigma in 
+  let (sp,evi) (* as evc *) = 
     try
       List.nth (Evarutil.non_instantiated sigma) (n-1) 
     with Failure _ -> 
-      error "not so many uninstantiated existential variables"
-  in 
-  let e_info = Evd.map sigma sp in
-  let env = Evarutil.evar_env e_info in
+      error "not so many uninstantiated existential variables" in 
+  let env = Evd.evar_env evi in
   let rawc = Constrintern.interp_rawconstr sigma env com in 
-  let wc' = w_refine sp rawc wc in
-  change_constraints_pftreestate wc'.sigma pfts
+  let evd = create_evar_defs sigma in
+  let evd' = w_refine env sp rawc evd in
+  change_constraints_pftreestate (evars_of evd') pfts