backtrack dans l'algo d'unification

fichier usage incorrect (libdir et bindir ont disparu)


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

1 files changed, 24 insertions, 40 deletions

diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 5f2c2716b..f791f3aba 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -14,59 +14,43 @@ open Term
 open Sign
 open Environ
 open Evd
-open Proof_trees
-open Proof_type
 open Refiner
+open Proof_type
 (*i*)
 
-(* Refinement of existential variables. *)
+type wc = named_context sigma (* for a better reading of the following *)
 
-val rc_of_pfsigma : proof_tree sigma -> named_context sigma
-val rc_of_glsigma : goal sigma -> named_context sigma
+(* Refinement of existential variables. *)
 
-(* a [walking_constraints] is a structure associated to a specific
-   goal; it collects all evars of which the goal depends.
-  It has the following structure:
-  [(identifying stamp, time stamp, 
-  { focus : set of evars among decls of which the goal depends;
-    hyps  : context of the goal;
-    decls : a superset of evars of which the goal may depend })]
-*)
+val rc_of_pfsigma : proof_tree sigma -> wc
+val rc_of_glsigma : goal sigma -> wc
 
 (* 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           = named_context sigma -> named_context sigma
+   a goal depend, either by instantiating one, or by declaring a new
+   dependent goal *)
+type w_tactic = wc -> wc
 
-val local_Constraints : 
-  goal sigma -> goal list sigma * validation
+val local_Constraints : tactic
 
-val startWalk : 
-  goal sigma -> named_context sigma * (named_context sigma -> tactic)
-
-val extract_decl : evar -> named_context sigma -> named_context sigma
-
-val restore_decl : evar -> evar_info -> named_context sigma -> named_context sigma
-
-(*i val w_Focusing_THEN : 
-  evar -> 'a result_w_tactic -> ('a -> w_tactic) -> w_tactic i*)
+val startWalk : goal sigma -> wc * (wc -> tactic)
 
+val extract_decl : evar -> w_tactic
+val restore_decl : evar -> evar_info -> w_tactic
 val w_Declare    : evar -> types -> w_tactic
 val w_Define     : evar -> constr -> w_tactic
 
-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_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_evar      : named_context sigma -> existential_key -> bool
+val w_Underlying : wc -> evar_map
+val w_env        : wc -> env
+val w_hyps       : wc -> named_context
+val w_whd        : wc -> constr -> constr
+val w_type_of    : wc -> constr -> constr
+val w_add_sign   : (identifier * types) -> w_tactic
+
+val w_whd_betadeltaiota : wc -> constr -> constr
+val w_hnf_constr        : wc -> constr -> constr
+val w_conv_x            : wc -> constr -> constr -> bool
+val w_const_value       : wc -> constant -> constr
+val w_defined_evar      : wc -> existential_key -> bool
 
 val instantiate : evar -> constr -> tactic
 val instantiate_tac : tactic_arg list -> tactic