premiere reorganisation de l\'unification

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

8 files changed, 24 insertions, 23 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 22cc44766..651b976c7 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -604,8 +604,7 @@ let priority l = List.map snd (List.filter (fun (pr,_) -> pr = 0) l)
 (* Try unification with the precompiled clause, then use registered Apply *)
 
 let unify_resolve (c,clenv) gls = 
-  let (wc,kONT) = startWalk gls in
-  let clenv' = connect_clenv wc clenv in
+  let clenv' = connect_clenv gls clenv in
   let _ = clenv_unique_resolver false clenv' gls in  
   h_simplest_apply c gls
 
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index c65126bbb..fc9bd3aa2 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -32,7 +32,7 @@ open Rawterm
 
 let e_give_exact c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in 
   if occur_existential t1 or occur_existential t2 then 
-     tclTHEN (unify t1) (exact_check c) gl
+     tclTHEN (Clenvtac.unify t1) (exact_check c) gl
   else exact_check c gl
 
 let assumption id = e_give_exact (mkVar id)
@@ -44,7 +44,7 @@ let e_resolve_with_bindings_tac  (c,lbind) gl =
   let (wc,kONT) = startWalk gl in
   let t = w_hnf_constr wc (w_type_of wc c) in 
   let clause = make_clenv_binding_apply wc (-1) (c,t) lbind in 
-  e_res_pf kONT clause gl
+  Clenvtac.e_res_pf kONT clause gl
 
 let e_resolve_constr c gls = e_resolve_with_bindings_tac (c,NoBindings) gls
 			     
@@ -192,8 +192,7 @@ open Auto
 (***************************************************************************)
 
 let unify_e_resolve  (c,clenv) gls = 
-  let (wc,kONT) = startWalk gls in
-  let clenv' = connect_clenv wc clenv in
+  let clenv' = connect_clenv gls clenv in
   let _ = clenv_unique_resolver false clenv' gls in
   vernac_e_resolve_constr c gls
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index a7e8c356e..bfedc8220 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -20,7 +20,6 @@ open Inductiveops
 open Environ
 open Libnames
 open Reductionops
-open Instantiate
 open Typeops
 open Typing
 open Retyping
@@ -585,7 +584,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty (dFLT,dFLTty) =
       let rty = beta_applist(p_i_minus_1,[ev]) in
       let tuple_tail = sigrec_clausal_form (siglen-1) rty in
       match
-	Instantiate.existential_opt_value (Evarutil.evars_of isevars) 
+	Evd.existential_opt_value (Evarutil.evars_of isevars) 
 	(destEvar ev)
       with
 	| Some w -> applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
diff --git a/tactics/inv.ml b/tactics/inv.ml
index fbdd790e0..e74fc05a9 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -46,7 +46,7 @@ let collect_meta_variables c =
 
 let check_no_metas clenv ccl =
   if occur_meta ccl then
-    let metas = List.map (fun n -> Metamap.find n clenv.namenv)
+    let metas = List.map (fun n -> Evd.Metamap.find n clenv.namenv)
 		  (collect_meta_variables ccl) in
     errorlabstrm "inversion" 
       (str ("Cannot find an instantiation for variable"^
@@ -112,7 +112,7 @@ let make_inv_predicate env sigma indf realargs id status concl =
               | None ->
 		let sort = get_sort_of env sigma concl in
 		let p = make_arity env true indf sort in
-		abstract_list_all env sigma p concl (realargs@[mkVar id]) in
+		Unification.abstract_list_all env sigma p concl (realargs@[mkVar id]) in
 	  let hyps,bodypred = decompose_lam_n_assum (nrealargs+1) pred in
 	  (* We lift to make room for the equations *)
 	  (hyps,lift nrealargs bodypred)
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 19c10fd72..95546142f 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -290,7 +290,7 @@ let lemInv id c gls =
     let (wc,kONT) = startWalk gls in
     let clause = mk_clenv_type_of wc c in
     let clause = clenv_constrain_with_bindings [(-1,mkVar id)] clause in
-    elim_res_pf kONT clause true gls
+    Clenvtac.elim_res_pf kONT clause true gls
   with 
     |  UserError (a,b) -> 
 	 errorlabstrm "LemInv" 
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index a5f5f742d..f092861f1 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -800,9 +800,12 @@ let apply_coq_setoid_rewrite hole_relation c1 c2 (lft2rgt,h) m =
 let relation_rewrite c1 c2 (lft2rgt,cl) gl =
  let but = pf_concl gl in
  let (hyp,c1,c2) =
-  let (cl',_) = Clenv.unify_to_subterm cl (c1,but) in
-  let c1 = Clenv.clenv_instance_term cl' c1 in
-  let c2 = Clenv.clenv_instance_term cl' c2 in
+   let cl' =
+     Clenv.clenv_wtactic
+       (fun evd -> fst (Unification.w_unify_to_subterm (pf_env gl) (c1,but) evd))
+       cl in
+   let c1 = Clenv.clenv_instance_term cl' c1 in
+   let c2 = Clenv.clenv_instance_term cl' c2 in
    (lft2rgt,Clenv.clenv_instance_template cl'), c1, c2
  in
   let input_relation = relation_of_hypothesis_and_term_to_rewrite gl hyp c1 in
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 1dbfbf17f..0e10a0b5d 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -22,6 +22,7 @@ open Libnames
 open Refiner
 open Tacmach
 open Clenv
+open Clenvtac
 open Pattern
 open Matching
 open Evar_refiner
@@ -173,8 +174,7 @@ let clause_type cls gl =
 (* Functions concerning matching of clausal environments *)
 
 let pf_is_matching gls pat n =
-  let (wc,_) = startWalk gls in 
-  is_matching_conv (w_env wc) (w_Underlying wc) pat n
+  is_matching_conv (pf_env gls) (project gls) pat n
 
 let pf_matches gls pat n =
   matches_conv (pf_env gls) (project gls) pat n
@@ -329,12 +329,12 @@ let general_elim_then_using
   let indclause' = clenv_constrain_with_bindings indbindings indclause in
   let elimclause = mk_clenv_from () (elim,w_type_of wc elim) in
   let indmv = 
-    match kind_of_term (last_arg (clenv_template elimclause).rebus) with
+    match kind_of_term (last_arg elimclause.templval.Evd.rebus) with
       | Meta mv -> mv
       | _         -> error "elimination"
   in
   let pmv =
-    let p, _ = decompose_app (clenv_template_type elimclause).rebus in
+    let p, _ = decompose_app elimclause.templtyp.Evd.rebus in
     match kind_of_term p with
       | Meta p -> p
       | _ ->
@@ -351,7 +351,7 @@ let general_elim_then_using
   let branchsigns = compute_construtor_signatures isrec ity in
   let brnames = compute_induction_names (Array.length branchsigns) allnames in
   let after_tac ce i gl =
-    let (hd,largs) = decompose_app (clenv_template_type ce).rebus in
+    let (hd,largs) = decompose_app ce.templtyp.Evd.rebus in
     let ba = { branchsign = branchsigns.(i);
                branchnames = brnames.(i);
                nassums = 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 655a5b53e..d5d972111 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -31,6 +31,7 @@ open Proof_type
 open Logic
 open Evar_refiner
 open Clenv
+open Clenvtac
 open Refiner
 open Tacticals
 open Hipattern
@@ -438,8 +439,8 @@ let bring_hyps hyps =
 let apply_with_bindings (c,lbind) gl = 
   let apply = 
     match kind_of_term c with 
-      | Lambda _ -> res_pf_cast 
-      | _ -> res_pf 
+      | Lambda _ -> Clenvtac.res_pf_cast 
+      | _ -> Clenvtac.res_pf 
   in 
   let (wc,kONT) = startWalk gl in
   (* The actual type of the theorem. It will be matched against the
@@ -452,13 +453,13 @@ let apply_with_bindings (c,lbind) gl =
       if n<0 then error "Apply: theorem has not enough premisses.";
       let clause = make_clenv_binding_apply wc n (c,thm_ty) lbind in
       apply kONT clause gl
-    with (RefinerError _|UserError _|Failure _) as exn ->
+    with (Pretype_errors.PretypeError _|RefinerError _|UserError _|Failure _) as exn ->
       let red_thm =
         try red_product (w_env wc) (w_Underlying wc) thm_ty
         with (Redelimination | UserError _) -> raise exn in
       try_apply red_thm in
   try try_apply thm_ty0
-  with (RefinerError _|UserError _|Failure _) ->
+  with (Pretype_errors.PretypeError _|RefinerError _|UserError _|Failure _) ->
     (* Last chance: if the head is a variable, apply may try
        second order unification *)
     let clause = make_clenv_binding_apply wc (-1) (c,thm_ty0) lbind in