Suite de la suppression : enamed_declaration est remplace par evar_map.

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

11 files changed, 20 insertions, 44 deletions

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index fe809b624..45c57eff4 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -32,7 +32,7 @@ type 'a result_w_tactic = walking_constraints -> walking_constraints * 'a
 type w_tactic = walking_constraints -> walking_constraints
 
 
-let local_Constraints lc gs = refiner Change_evars gs
+let local_Constraints gs = refiner Change_evars gs
 
 let startWalk gls =
   let evc = project_with_focus gls in
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 13a4a5e41..7100e9844 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -42,7 +42,7 @@ dependent goal *)
 type w_tactic           = walking_constraints -> walking_constraints
 
 val local_Constraints : 
-  local_constraints -> goal sigma -> goal list sigma * validation
+  goal sigma -> goal list sigma * validation
 
 val startWalk : 
   goal sigma -> walking_constraints * (walking_constraints -> tactic)
@@ -55,7 +55,7 @@ val w_Focusing_THEN :
 val w_Declare    : evar -> types -> w_tactic
 val w_Define     : evar -> constr -> w_tactic
 
-val w_Underlying : walking_constraints -> enamed_declarations
+val w_Underlying : walking_constraints -> evar_map
 val w_env        : walking_constraints -> env
 val w_hyps       : walking_constraints -> named_context
 val w_whd        : walking_constraints -> constr -> constr
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index cd63d419e..462134fce 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -104,11 +104,11 @@ val get_pftreestate : unit -> pftreestate
    the current focused proof or raises a [UserError] if there is no
    focused proof or if there is no more subgoals *)
 
-val get_goal_context : int -> enamed_declarations * env
+val get_goal_context : int -> Evd.evar_map * env
 
 (* [get_current_goal_context ()] works as [get_goal_context 1] *)
 
-val get_current_goal_context : unit -> enamed_declarations * env
+val get_current_goal_context : unit -> Evd.evar_map * env
 
 (*s [get_current_proof_name ()] return the name of the current focused
     proof or failed if no proof is focused *)
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index c6a1df1d9..429e93aa4 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -66,22 +66,12 @@ let is_tactic_proof pf = (pf.subproof <> None)
 (*            Constraints for existential variables                *)
 (*******************************************************************)
 
-(* A local constraint is just a set of section_paths *)
-
-(* recall : type local_constraints = Intset.t *)
-
-(* A global constraint is a mappings of existential variables
-   with some extra information for the program and mimick
-   tactics. *)
-
-type global_constraints  = enamed_declarations timestamped
-
 (* A readable constraint is a global constraint plus a focus set
    of existential variables and a signature. *)
 
 type evar_recordty = {
   hyps  : named_context;
-  decls : enamed_declarations }
+  decls : evar_map }
 
 and readable_constraints = evar_recordty timestamped
 
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index 00f51fcca..4ad1509fe 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -34,18 +34,12 @@ val is_complete_proof : proof_tree -> bool
 val is_leaf_proof     : proof_tree -> bool
 val is_tactic_proof   : proof_tree -> bool
 
-
-(*s A global constraint is a mappings of existential variables with
-    some extra information for the program and mimick tactics. *)
-
-type global_constraints = enamed_declarations timestamped
-
 (*s A readable constraint is a global constraint plus a focus set
     of existential variables and a signature. *)
 
 type evar_recordty = {
   hyps  : named_context;
-  decls : enamed_declarations }
+  decls : evar_map }
 
 and readable_constraints = evar_recordty timestamped
 
@@ -53,7 +47,7 @@ val rc_of_gc  : global_constraints -> goal -> readable_constraints
 val rc_add    : readable_constraints -> int * goal -> readable_constraints
 val get_hyps  : readable_constraints -> named_context
 val get_env   : readable_constraints -> env
-val get_decls : readable_constraints -> enamed_declarations
+val get_decls : readable_constraints -> evar_map
 val get_gc    : readable_constraints -> global_constraints
 val remap     : readable_constraints -> int * goal -> readable_constraints
 
@@ -80,7 +74,7 @@ val prgl         : goal -> std_ppcmds
 val pr_seq       : goal -> std_ppcmds
 val pr_evars     : (int * goal) list -> std_ppcmds
 val pr_evars_int : int -> (int * goal) list -> std_ppcmds
-val pr_subgoals_existential : enamed_declarations -> goal list -> std_ppcmds
+val pr_subgoals_existential : evar_map -> goal list -> std_ppcmds
 
 (* Gives the ast corresponding to a tactic argument *)
 val ast_of_cvt_arg : tactic_arg ->  Coqast.t 
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index c866d85ed..81c57e539 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -55,13 +55,9 @@ type prim_rule = {
   params : Coqast.t list;
   terms : constr list }
 
-type local_constraints = Intset.t
-
-type enamed_declarations = evar_map
-
 (* A global constraint is a mappings of existential variables
    with some extra information for the program tactic *)
-type global_constraints  = enamed_declarations timestamped
+type global_constraints  = evar_map timestamped
 
 (* Signature useful to define the tactic type *)
 type 'a sigma = { 
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 3d972da3f..2c57806b5 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -58,13 +58,9 @@ type prim_rule = {
   params : Coqast.t list;
   terms : constr list }
 
-type local_constraints = Intset.t
-
-type enamed_declarations = evar_map
-
 (* A global constraint is a mappings of existential variables
    with some extra information for the program tactic *)
-type global_constraints  = enamed_declarations timestamped
+type global_constraints  = evar_map timestamped
 
 (* The type [goal sigma] is the type of subgoal. It has the following form
 \begin{verbatim}
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 290c7debc..4c9fade3e 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -117,7 +117,7 @@ type pftreestate
 val proof_of_pftreestate : pftreestate -> proof_tree
 val cursor_of_pftreestate : pftreestate -> int list
 val is_top_pftreestate : pftreestate -> bool
-val evc_of_pftreestate : pftreestate -> enamed_declarations
+val evc_of_pftreestate : pftreestate -> Evd.evar_map
 val top_goal_of_pftreestate : pftreestate -> goal sigma
 val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
 
@@ -150,10 +150,10 @@ val change_constraints_pftreestate
 open Pp
 (*i*)
 
-val print_proof : enamed_declarations -> named_context -> proof_tree -> std_ppcmds
+val print_proof : Evd.evar_map -> named_context -> proof_tree -> std_ppcmds
 val pr_rule      : rule -> std_ppcmds
 val pr_tactic    : tactic_expression -> std_ppcmds
 val print_script :
-  bool -> enamed_declarations -> named_context -> proof_tree -> std_ppcmds
+  bool -> Evd.evar_map -> named_context -> proof_tree -> std_ppcmds
 val print_treescript :
-  enamed_declarations -> named_context -> proof_tree -> std_ppcmds
+  Evd.evar_map -> named_context -> proof_tree -> std_ppcmds
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index b037a4a31..32d96bce1 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -52,7 +52,7 @@ type value =
 
 (* Signature for interpretation: val_interp and interpretation functions *)
 and interp_sign =
-  { evc : enamed_declarations;
+  { evc : Evd.evar_map;
     env : Environ.env;
     lfun : (identifier * value) list;
     lmatch : (int * constr) list;
diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli
index 9a979ea74..631d7e0af 100644
--- a/proofs/tacinterp.mli
+++ b/proofs/tacinterp.mli
@@ -31,7 +31,7 @@ type value =
 
 (* Signature for interpretation: val\_interp and interpretation functions *)
 and interp_sign =
-  { evc : enamed_declarations;
+  { evc : Evd.evar_map;
     env : Environ.env;
     lfun : (identifier * value) list;
     lmatch : (int * constr) list;
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 48dcb2368..6a2ca4414 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -28,7 +28,7 @@ type tactic     = Proof_type.tactic;;
 
 val sig_it  : 'a sigma   -> 'a
 val sig_sig : goal sigma -> global_constraints
-val project : goal sigma -> enamed_declarations
+val project : goal sigma -> Evd.evar_map
 
 val re_sig : 'a -> global_constraints -> 'a sigma
 
@@ -63,7 +63,7 @@ val pf_reduction_of_redexp : goal sigma -> red_expr -> constr -> constr
 
 
 val pf_reduce : 
-  (env -> enamed_declarations -> constr -> constr) ->
+  (env -> Evd.evar_map -> constr -> constr) ->
     goal sigma -> constr -> constr
 
 val pf_whd_betadeltaiota       : goal sigma -> constr -> constr
@@ -94,7 +94,7 @@ type pftreestate
 val proof_of_pftreestate    : pftreestate -> proof_tree
 val cursor_of_pftreestate   : pftreestate -> int list
 val is_top_pftreestate      : pftreestate -> bool
-val evc_of_pftreestate      : pftreestate -> enamed_declarations
+val evc_of_pftreestate      : pftreestate -> Evd.evar_map
 val top_goal_of_pftreestate : pftreestate -> goal sigma
 val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
 val traverse                : int -> pftreestate -> pftreestate