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

6 files changed, 15 insertions, 89 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
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 4766d94cbf..57312cb4b7 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -11,23 +11,14 @@
 (*i*)
 open Names
 open Term
-open Sign
 open Environ
 open Evd
 open Refiner
-open Proof_type
 (*i*)
 
-type wc = named_context sigma (* for a better reading of the following *)
-
 (* Refinement of existential variables. *)
 
-(* 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_refine :  evar -> Rawterm.rawconstr  -> w_tactic
+val w_refine :  env -> evar -> Rawterm.rawconstr  -> evar_defs -> evar_defs
 
 val instantiate_pf_com :
   int -> Topconstr.constr_expr -> pftreestate -> pftreestate
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 967b3edaf5..445e19967a 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -70,25 +70,6 @@ let is_tactic_proof pf = match pf.ref with
 (*            Constraints for existential variables                *)
 (*******************************************************************)
 
-(* A readable constraint is a global constraint plus a focus set
-   of existential variables and a signature. *)
-
-(* Functions on readable constraints *)
-			     
-let mt_evcty gc = 
-  { it = empty_named_context; sigma = gc }
-
-let rc_of_gc evds gl = 
-  { it = gl.evar_hyps; sigma = evds }
-
-let rc_add evc (k,v) = 
-  { it  = evc.it;
-    sigma = Evd.add evc.sigma k v }
-
-let get_hyps  evc = evc.it
-let get_env   evc = Global.env_of_context evc.it
-let get_gc    evc = evc.sigma
-
 let pf_lookup_name_as_renamed env ccl s =
   Detyping.lookup_name_as_renamed env ccl s
 
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index 348a4b173f..12f82b7f48 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -33,16 +33,6 @@ val is_complete_proof : proof_tree -> bool
 val is_leaf_proof     : proof_tree -> bool
 val is_tactic_proof   : proof_tree -> bool
 
-(*s A readable constraint is a global constraint plus a focus set
-    of existential variables and a signature. *)
-
-val rc_of_gc  : evar_map -> goal -> named_context sigma
-val rc_add    : named_context sigma -> existential_key * goal -> 
-  named_context sigma
-val get_hyps  : named_context sigma -> named_context
-val get_env   : named_context sigma -> env
-val get_gc    : named_context sigma -> evar_map
-
 val pf_lookup_name_as_renamed  : env -> constr -> identifier -> int option
 val pf_lookup_index_as_renamed : env -> constr -> int -> int option
 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index b2629013b1..acdc302aff 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -31,8 +31,6 @@ let sig_it x = x.it
 let sig_sig x = x.sigma
 
 
-let project_with_focus gls = rc_of_gc (gls.sigma) (gls.it)
-
 let pf_status pf = pf.open_subgoals
 
 let is_complete pf = (0 = (pf_status pf))
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index f6f65ef938..8e39e0181c 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -23,8 +23,6 @@ open Tacexpr
 val sig_it  : 'a sigma -> 'a
 val sig_sig : 'a sigma -> evar_map
 
-val project_with_focus : goal sigma -> named_context sigma
-
 val unpackage : 'a sigma -> evar_map ref * 'a
 val repackage : evar_map ref -> 'a -> 'a sigma
 val apply_sig_tac :