unification encore...

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

10 files changed, 37 insertions, 41 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 651b976c7..0dc0a9f4c 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -44,10 +44,10 @@ open Tacexpr
 (****************************************************************************)
 
 type auto_tactic = 
-  | Res_pf     of constr * unit clausenv (* Hint Apply *)
-  | ERes_pf    of constr * unit clausenv (* Hint EApply *)
+  | Res_pf     of constr * wc clausenv (* Hint Apply *)
+  | ERes_pf    of constr * wc clausenv (* Hint EApply *)
   | Give_exact of constr                  
-  | Res_pf_THEN_trivial_fail of constr * unit clausenv (* Hint Immediate *)
+  | Res_pf_THEN_trivial_fail of constr * wc clausenv (* Hint Immediate *)
   | Unfold_nth of global_reference       (* Hint Unfold *)
   | Extern     of glob_tactic_expr       (* Hint Extern *) 
 
@@ -186,11 +186,15 @@ let make_exact_entry name (c,cty) =
 	(head_of_constr_reference (List.hd (head_constr cty)),
 	   { hname=name; pri=0; pat=None; code=Give_exact c })
 
+let dummy_goal =
+  {it={evar_hyps=empty_named_context;evar_concl=mkProp;evar_body=Evar_empty};
+   sigma=Evd.empty}
+
 let make_apply_entry env sigma (eapply,verbose) name (c,cty) =
   let cty = hnf_constr env sigma cty in
   match kind_of_term cty with
     | Prod _ ->
-        let ce = mk_clenv_from () (c,cty) in
+        let ce = mk_clenv_from dummy_goal (c,cty) in
 	let c' = (clenv_template_type ce).rebus in
 	let pat = Pattern.pattern_of_constr c' in
         let hd = (try head_pattern_bound pat
@@ -256,7 +260,7 @@ let make_extern name pri pat tacast =
 let make_trivial env sigma (name,c) =
   let t = hnf_constr env sigma (type_of env sigma c) in
   let hd = head_of_constr_reference (List.hd (head_constr t)) in
-  let ce = mk_clenv_from () (c,t) in
+  let ce = mk_clenv_from dummy_goal (c,t) in
   (hd, { hname = name;
 	       pri=1;
                pat = Some (Pattern.pattern_of_constr (clenv_template_type ce).rebus);
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 80b807908..18daa6ebe 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -24,10 +24,10 @@ open Vernacexpr
 (*i*)
   
 type auto_tactic = 
-  | Res_pf     of constr * unit clausenv    (* Hint Apply *)
-  | ERes_pf    of constr * unit clausenv    (* Hint EApply *)
+  | Res_pf     of constr * wc clausenv    (* Hint Apply *)
+  | ERes_pf    of constr * wc clausenv    (* Hint EApply *)
   | Give_exact of constr                  
-  | Res_pf_THEN_trivial_fail of constr * unit clausenv (* Hint Immediate *)
+  | Res_pf_THEN_trivial_fail of constr * wc clausenv (* Hint Immediate *)
   | Unfold_nth of global_reference          (* Hint Unfold *)
   | Extern     of Tacexpr.glob_tactic_expr   (* Hint Extern *)
 
@@ -139,7 +139,7 @@ val priority : (int * 'a) list -> 'a list
 val default_search_depth : int ref
 
 (* Try unification with the precompiled clause, then use registered Apply *)
-val unify_resolve : (constr * unit clausenv) -> tactic
+val unify_resolve : (constr * wc clausenv) -> tactic
 
 (* [ConclPattern concl pat tacast]:
    if the term concl matches the pattern pat, (in sense of 
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 700c8fed7..64188d3b8 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -42,7 +42,7 @@ let e_assumption gl =
 
 let e_resolve_with_bindings_tac  (c,lbind) gl = 
   let t = pf_hnf_constr gl (pf_type_of gl c) in 
-  let clause = make_clenv_binding_apply (rc_of_glsigma gl) (-1) (c,t) lbind in 
+  let clause = make_clenv_binding_apply gl (-1) (c,t) lbind in 
   Clenvtac.e_res_pf clause gl
 
 let e_resolve_constr c gls = e_resolve_with_bindings_tac (c,NoBindings) gls
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index a58f61550..b5a0370c7 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -66,8 +66,8 @@ let instantiate_tac = function
 *)
 
 let let_evar nam typ gls =
-  let wc = Refiner.project_with_focus gls in
   let sp = Evarutil.new_evar () in
-  let wc' = w_Declare sp typ wc in
-  let ngls = {gls with sigma = wc'.sigma} in
+  let mm = (Evarutil.create_evar_defs gls.sigma, Metamap.empty) in
+  let (evd,_) = Unification.w_Declare (pf_env gls) sp typ mm in
+  let ngls = {gls with sigma = Evarutil.evars_of evd} in
     Tactics.forward true nam (mkEvar(sp,[||])) ngls 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 7c4456b3d..9a02ba608 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -446,7 +446,7 @@ let raw_inversion inv_kind indbinding id status names gl =
   let env = pf_env gl and sigma = project gl in
   let c = mkVar id in
   let t = strong_prodspine (pf_whd_betadeltaiota gl) (pf_type_of gl c) in
-  let indclause = mk_clenv_from (rc_of_glsigma gl) (c,t) in
+  let indclause = mk_clenv_from gl (c,t) in
   let indclause' = clenv_constrain_with_bindings indbinding indclause in
   let newc = clenv_instance_template indclause' in
   let ccl = clenv_instance_template_type indclause' in
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 118481547..aa980fd47 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -287,7 +287,7 @@ let add_inversion_lemma_exn na com comsort bool tac =
 
 let lemInv id c gls =
   try
-    let clause = mk_clenv_type_of (rc_of_glsigma gls) c in
+    let clause = mk_clenv_type_of gls c in
     let clause = clenv_constrain_with_bindings [(-1,mkVar id)] clause in
     Clenvtac.elim_res_pf clause true gls
   with 
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 081f135c6..aacaa050e 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -969,9 +969,7 @@ let relation_rewrite c1 c2 (lft2rgt,cl) gl =
 
 let general_s_rewrite lft2rgt c gl =
  let ctype = pf_type_of gl c in
- let eqclause  =
-  Clenv.make_clenv_binding
-    (Evar_refiner.rc_of_glsigma gl) (c,ctype) Rawterm.NoBindings in
+ let eqclause  = Clenv.make_clenv_binding gl (c,ctype) Rawterm.NoBindings in
  let (equiv, args) =
   decompose_app (Clenv.clenv_instance_template_type eqclause) in
  let rec get_last_two = function
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 72ec0bd2e..fa5eeaef3 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -324,9 +324,9 @@ let general_elim_then_using
   elim isrec allnames tac predicate (indbindings,elimbindings) c gl =
   let (ity,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
   (* applying elimination_scheme just a little modified *)
-  let indclause  = mk_clenv_from (rc_of_glsigma gl) (c,t) in
+  let indclause  = mk_clenv_from gl (c,t) in
   let indclause' = clenv_constrain_with_bindings indbindings indclause in
-  let elimclause = mk_clenv_from () (elim,pf_type_of gl elim) in
+  let elimclause = mk_clenv_from gl (elim,pf_type_of gl elim) in
   let indmv = 
     match kind_of_term (last_arg elimclause.templval.Evd.rebus) with
       | Meta mv -> mv
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6fe3d75af..d64c90916 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -445,13 +445,12 @@ let apply_with_bindings (c,lbind) gl =
   (* The actual type of the theorem. It will be matched against the
   goal. If this fails, then the head constant will be unfolded step by
   step. *)
-  let wc = rc_of_glsigma gl in
   let thm_ty0 = nf_betaiota (pf_type_of gl c) in
   let rec try_apply thm_ty =
     try
       let n = nb_prod thm_ty - nb_prod (pf_concl gl) in
       if n<0 then error "Apply: theorem has not enough premisses.";
-      let clause = make_clenv_binding_apply wc n (c,thm_ty) lbind in
+      let clause = make_clenv_binding_apply gl n (c,thm_ty) lbind in
       apply clause gl
     with (Pretype_errors.PretypeError _|RefinerError _|UserError _|Failure _) as exn ->
       let red_thm =
@@ -462,7 +461,7 @@ let apply_with_bindings (c,lbind) gl =
   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 
+    let clause = make_clenv_binding_apply gl (-1) (c,thm_ty0) lbind in 
     apply clause gl
 
 let apply c = apply_with_bindings (c,NoBindings)
@@ -474,7 +473,7 @@ let apply_list = function
 (* Resolution with no reduction on the type *)
 
 let apply_without_reduce c gl = 
-  let clause = mk_clenv_type_of (rc_of_glsigma gl) c in 
+  let clause = mk_clenv_type_of gl c in 
   res_pf clause gl
 
 (* A useful resolution tactic which, if c:A->B, transforms |- C into
@@ -830,8 +829,7 @@ let rec intros_clearing = function
 (* Adding new hypotheses  *)
 
 let new_hyp mopt (c,lbind) g =
-  let clause  =
-    make_clenv_binding (rc_of_glsigma g) (c,pf_type_of g c) lbind in
+  let clause  = make_clenv_binding g (c,pf_type_of g c) lbind in
   let (thd,tstack) = whd_stack (clenv_instance_template clause) in
   let nargs = List.length tstack in
   let cut_pf = 
@@ -926,10 +924,9 @@ let type_clenv_binding wc (c,t) lbind =
 let general_elim (c,lbindc) (elimc,lbindelimc) ?(allow_K=true) gl = 
   let ct = pf_type_of gl c in
   let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
-  let indclause  = make_clenv_binding (rc_of_glsigma gl) (c,t) lbindc  in
+  let indclause  = make_clenv_binding gl (c,t) lbindc  in
   let elimt      = pf_type_of gl elimc in
-  let elimclause =
-    make_clenv_binding (rc_of_glsigma gl) (elimc,elimt) lbindelimc in 
+  let elimclause = make_clenv_binding gl (elimc,elimt) lbindelimc in 
   elimination_clause_scheme elimclause indclause allow_K gl
 
 (* Elimination tactic with bindings but using the default elimination 
@@ -971,7 +968,7 @@ let simplest_elim c = default_elim (c,NoBindings)
 
 (* Elimination in hypothesis *)
 
-let elimination_in_clause_scheme id elimclause indclause =
+let elimination_in_clause_scheme id elimclause indclause gl =
   let (hypmv,indmv) = 
     match clenv_independent elimclause with
         [k1;k2] -> (k1,k2)
@@ -981,7 +978,7 @@ let elimination_in_clause_scheme id elimclause indclause =
   let hyp = mkVar id in
   let hyp_typ = clenv_type_of elimclause' hyp in
   let hypclause =
-    mk_clenv_from_n elimclause'.hook (Some 0) (hyp, hyp_typ) in
+    mk_clenv_from_n gl (Some 0) (hyp, hyp_typ) in
   let elimclause'' = clenv_fchain hypmv elimclause' hypclause in  
   let new_hyp_prf  = clenv_instance_template elimclause'' in
   let new_hyp_typ  = clenv_instance_template_type elimclause'' in
@@ -995,16 +992,14 @@ let elimination_in_clause_scheme id elimclause indclause =
       [ (* Try to insert the new hyp at the same place *)
         tclORELSE (intro_replacing id)
           (tclTHEN (clear [id]) (introduction id));
-        refine_no_check new_hyp_prf])
+        refine_no_check new_hyp_prf]) gl
 
 let general_elim_in id (c,lbindc) (elimc,lbindelimc) gl = 
   let ct = pf_type_of gl c in
   let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
-  let indclause  =
-    make_clenv_binding (rc_of_glsigma gl) (c,t) lbindc  in
+  let indclause  = make_clenv_binding gl (c,t) lbindc  in
   let elimt      = pf_type_of gl elimc in
-  let elimclause =
-    make_clenv_binding (rc_of_glsigma gl) (elimc,elimt) lbindelimc in 
+  let elimclause = make_clenv_binding gl (elimc,elimt) lbindelimc in 
   elimination_in_clause_scheme id elimclause indclause gl
 
 (* Case analysis tactics *)
@@ -1376,10 +1371,9 @@ let cook_sign hyp0 indvars env =
 
 let induction_tac varname typ ((elimc,lbindelimc),elimt) gl =
   let c = mkVar varname in
-  let wc = rc_of_glsigma gl in
-  let indclause  = make_clenv_binding wc (c,typ) NoBindings  in
+  let indclause  = make_clenv_binding gl (c,typ) NoBindings  in
   let elimclause =
-    make_clenv_binding wc (mkCast (elimc,elimt),elimt) lbindelimc in
+    make_clenv_binding gl (mkCast (elimc,elimt),elimt) lbindelimc in
   elimination_clause_scheme elimclause indclause true gl
 
 let make_up_names7 n ind (old_style,cname) = 
@@ -1667,7 +1661,7 @@ let simple_destruct = function
  *)
 
 let elim_scheme_type elim t gl =
-  let clause = mk_clenv_type_of (rc_of_glsigma gl) elim in
+  let clause = mk_clenv_type_of gl elim in
   match kind_of_term (last_arg (clenv_template clause).rebus) with
     | Meta mv ->
         let clause' =
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 03e295d8f..d2a16dc8e 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -31,7 +31,7 @@ open Rawterm
 
 (*s General functions. *)
 
-val type_clenv_binding : named_context sigma ->
+val type_clenv_binding : goal sigma ->
   constr * constr -> constr bindings  -> constr
 
 val string_of_inductive : constr -> string