Suppression des stamps et donc des *_constraints

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

1 files changed, 19 insertions, 21 deletions

diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 7100e9844..9f09cfba5 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -21,8 +21,8 @@ open Refiner
 
 (* Refinement of existential variables. *)
 
-val rc_of_pfsigma : proof_tree sigma -> readable_constraints
-val rc_of_glsigma : goal sigma -> readable_constraints
+val rc_of_pfsigma : proof_tree sigma -> named_context sigma
+val rc_of_glsigma : goal sigma -> named_context sigma
 
 (* a [walking_constraints] is a structure associated to a specific
    goal; it collects all evars of which the goal depends.
@@ -32,20 +32,18 @@ val rc_of_glsigma : goal sigma -> readable_constraints
     hyps  : context of the goal;
     decls : a superset of evars of which the goal may depend })]
 *)
-type walking_constraints
-
-type 'a result_w_tactic = walking_constraints -> walking_constraints * 'a
+type 'a result_w_tactic = named_context sigma -> named_context sigma * 'a
 
 (* 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           = walking_constraints -> walking_constraints
+type w_tactic           = named_context sigma -> named_context sigma
 
 val local_Constraints : 
   goal sigma -> goal list sigma * validation
 
 val startWalk : 
-  goal sigma -> walking_constraints * (walking_constraints -> tactic)
+  goal sigma -> named_context sigma * (named_context sigma -> tactic)
 
 val walking_THEN    : 'a result_w_tactic -> ('a -> tactic) -> tactic
 val walking         : w_tactic -> tactic
@@ -55,23 +53,23 @@ val w_Focusing_THEN :
 val w_Declare    : evar -> types -> w_tactic
 val w_Define     : evar -> constr -> w_tactic
 
-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
-val w_type_of    : walking_constraints -> constr -> constr
-val w_add_sign   : (identifier * types) -> walking_constraints 
-                     -> walking_constraints
+val w_Underlying : named_context sigma -> evar_map
+val w_env        : named_context sigma -> env
+val w_hyps       : named_context sigma -> named_context
+val w_whd        : named_context sigma -> constr -> constr
+val w_type_of    : named_context sigma -> constr -> constr
+val w_add_sign   : (identifier * types) -> named_context sigma 
+                     -> named_context sigma
 
 val w_IDTAC      : w_tactic
 val w_ORELSE     : w_tactic -> w_tactic -> w_tactic
-val ctxt_type_of : readable_constraints -> constr -> constr
-val w_whd_betadeltaiota : walking_constraints -> constr -> constr
-val w_hnf_constr        : walking_constraints -> constr -> constr
-val w_conv_x            : walking_constraints -> constr -> constr -> bool
-val w_const_value       : walking_constraints -> constant -> constr
-val w_defined_const     : walking_constraints -> constant -> bool
-val w_defined_evar      : walking_constraints -> existential_key -> bool
+val ctxt_type_of : named_context sigma -> constr -> constr
+val w_whd_betadeltaiota : named_context sigma -> constr -> constr
+val w_hnf_constr        : named_context sigma -> constr -> constr
+val w_conv_x            : named_context sigma -> constr -> constr -> bool
+val w_const_value       : named_context sigma -> constant -> constr
+val w_defined_const     : named_context sigma -> constant -> bool
+val w_defined_evar      : named_context sigma -> existential_key -> bool
 
 val instantiate_pf     : int -> constr -> pftreestate -> pftreestate
 val instantiate_pf_com : int -> Coqast.t -> pftreestate -> pftreestate