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

4 files changed, 31 insertions, 56 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 0c76be8df..831267087 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -82,8 +82,6 @@ type 'a clausenv = {
   env : clbinding Intmap.t;
   hook : 'a }
 
-type wc = named_context sigma
-
 let applyHead n c wc = 
   let rec apprec n c cty wc =
     if n = 0 then 
@@ -133,7 +131,6 @@ let unify_r2l x = x
 let sort_eqns = unify_r2l
 
 
-
 let unify_0 cv_pb wc m n =
   let env = w_env wc
   and sigma = w_Underlying wc in
@@ -186,7 +183,8 @@ let unify_0 cv_pb wc m n =
   if (not(occur_meta m)) & is_fconv cv_pb env sigma m n then 
     ([],[])
   else 
-    unirec_rec cv_pb ([],[]) m n
+    let (mc,ec) = unirec_rec cv_pb ([],[]) m n in
+    (sort_eqns mc, sort_eqns ec)
 
 
 (* Unification
@@ -802,7 +800,7 @@ let clenv_unify allow_K cv_pb ty1 ty2 clenv =
            with ex when catchable_exception ex -> 
              error "Cannot solve a second-order unification problem")
 
-     | _ -> clenv_typed_unify cv_pb ty1 ty2 clenv
+     | _ -> clenv_unify_0 cv_pb ty1 ty2 clenv
 
 
 (* [clenv_bchain mv clenv' clenv]
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 2514b6e75..e83d8d7d7 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -53,8 +53,6 @@ type 'a clausenv = {
  * [hook] is the pointer to the current walking context, for
  *        integrating existential vars and metavars. *)
 
-type wc = named_context sigma (* for a better reading of the following *)
-
 val unify : constr -> tactic
 val unify_0 : 
   Reductionops.conv_pb -> wc -> constr -> constr 
@@ -99,16 +97,9 @@ val clenv_type_of : wc clausenv -> constr -> constr
 val clenv_unique_resolver : bool -> wc clausenv -> goal sigma -> wc clausenv
 
 val make_clenv_binding_apply :
-  named_context sigma ->
-  int ->
-  constr * constr ->
-  (bindOcc * types) list ->
-  named_context sigma clausenv
+  wc -> int -> constr * types -> constr substitution -> wc clausenv
 val make_clenv_binding :
-  named_context sigma ->
-  constr * constr ->
-  (bindOcc * types) list ->
-  named_context sigma clausenv
+  wc -> constr * types -> constr substitution -> wc clausenv
 
 (* Exported for program.ml only *)
 val clenv_add_sign : 
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 7b704b777..521cd9b4d 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -24,6 +24,8 @@ open Proof_type
 open Logic
 open Refiner
 
+type wc = named_context sigma (* for a better reading of the following *)
+
 let rc_of_pfsigma sigma = rc_of_gc sigma.sigma sigma.it.goal
 let rc_of_glsigma sigma = rc_of_gc sigma.sigma sigma.it
 
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