inclusion de meta_map dans evar_defs

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

10 files changed, 28 insertions, 33 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 66454059e3..c32130d2c0 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -323,7 +323,7 @@ let forward_subst_tactic =
 let set_extern_subst_tactic f = forward_subst_tactic := f
 
 let subst_autohint (_,subst,(local,name,hintlist as obj)) = 
-  let trans_clenv clenv = Clenv.subst_clenv (fun _ a -> a) subst clenv in
+  let trans_clenv clenv = Clenv.subst_clenv subst clenv in
   let trans_data data code = 	      
     { data with
 	pat = option_smartmap (subst_pattern subst) data.pat ;
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 38dc8f58e4..f9834f5229 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -821,7 +821,7 @@ let swap_equands gls eqn =
 let swapEquandsInConcl gls =
   let (lbeq,(t,e1,e2)) = find_eq_data_decompose (pf_concl gls) in
   let sym_equal = lbeq.sym in
-  refine (applist(sym_equal,[t;e2;e1;mkMeta (Clenv.new_meta())])) gls
+  refine (applist(sym_equal,[t;e2;e1;Evarutil.mk_new_meta()])) gls
 
 let swapEquandsInHyp id gls =
   ((tclTHENS (cut_replacing id (swap_equands gls (pf_get_hyp_typ gls id)))
@@ -880,8 +880,8 @@ let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
     else
       (build_non_dependent_rewrite_predicate (t,e1,e2)  body  gls)
   in
-  refine (applist(eq_elim,[t;e1;p;mkMeta(Clenv.new_meta());
-                           e2;mkMeta(Clenv.new_meta())])) gls
+  refine (applist(eq_elim,[t;e1;p;Evarutil.mk_new_meta();
+                           e2;Evarutil.mk_new_meta()])) gls
 
 (* [subst_tuple_term dep_pair B]
 
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index b5a0370c79..f2db79d1a2 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -67,7 +67,7 @@ let instantiate_tac = function
 
 let let_evar nam typ gls =
   let sp = Evarutil.new_evar () 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
+  let evd = Evarutil.create_evar_defs gls.sigma in
+  let evd' = Unification.w_Declare (pf_env gls) sp typ evd 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 0ac1203275..1e4267421b 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -475,7 +475,7 @@ let raw_inversion inv_kind indbinding id status names gl =
         (fun id ->
            (tclTHEN
               (apply_term (mkVar id)
-                 (list_tabulate (fun _ -> mkMeta(Clenv.new_meta())) neqns))
+                 (list_tabulate (fun _ -> Evarutil.mk_new_meta()) neqns))
               reflexivity))])
   gl
 
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index aa980fd47b..9fd54ee694 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -289,7 +289,7 @@ let lemInv id c gls =
   try
     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
+    Clenvtac.res_pf clause ~allow_K:true gls
   with 
     |  UserError (a,b) -> 
 	 errorlabstrm "LemInv" 
diff --git a/tactics/refine.ml b/tactics/refine.ml
index aa9cf2c570..88e2fcea81 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -92,7 +92,7 @@ and pp_sg sg =
 let replace_by_meta env gmm = function
   | TH (m, mm, sgp) when isMeta (strip_outer_cast m) -> m,mm,sgp
   | (TH (c,mm,_)) as th ->
-      let n = Clenv.new_meta() in
+      let n = Evarutil.new_meta() in
       let m = mkMeta n in
       (* quand on introduit une mv on calcule son type *)
       let ty = match kind_of_term c with
@@ -340,7 +340,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as th) gl =
 let refine oc gl =
   let sigma = project gl in
   let env = pf_env gl in
-  let (gmm,c) = Clenv.exist_to_meta sigma oc in
+  let (gmm,c) = Evarutil.exist_to_meta sigma oc in
   let th = compute_metamap env gmm c in
   tcc_aux [] th gl
 
diff --git a/tactics/refine.mli b/tactics/refine.mli
index 26cd04ef08..89e5316755 100644
--- a/tactics/refine.mli
+++ b/tactics/refine.mli
@@ -8,7 +8,6 @@
 
 (*i $Id$ i*)
 
-open Term
 open Tacmach
 
-val refine : Pretyping.open_constr -> tactic
+val refine : Evd.open_constr -> tactic
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 905ca60b45..853b4e2959 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -22,6 +22,8 @@ open Util
 open Pp
 open Printer
 open Environ
+open Clenv
+open Unification
 open Tactics 
 open Tacticals
 open Vernacexpr
@@ -919,7 +921,7 @@ let syntactic_but_representation_of_marked_but hole_relation =
        else
         let c_is_proper =
          let typ = mkApp (rel_out, [| c ; c |]) in
-          mkCast (mkMeta (Clenv.new_meta ()),typ)
+          mkCast (Evarutil.mk_new_meta (),typ)
         in
          mkApp ((Lazy.force coq_ProperElementToKeep),
           [| hole_relation ; Lazy.force coq_Left2Right; precise_out ;
@@ -958,9 +960,7 @@ let relation_rewrite c1 c2 (lft2rgt,cl) gl =
  let but = pf_concl gl in
  let (hyp,c1,c2) =
    let cl' =
-     Clenv.clenv_wtactic
-       (fun evd-> fst (Unification.w_unify_to_subterm (pf_env gl) (c1,but) evd))
-       cl in
+     {cl with env = fst (w_unify_to_subterm (pf_env gl) (c1,but) cl.env)} in
    let c1 = Clenv.clenv_nf_meta cl' c1 in
    let c2 = Clenv.clenv_nf_meta cl' c2 in
    (lft2rgt,Clenv.clenv_value cl'), c1, c2
@@ -974,7 +974,7 @@ let relation_rewrite c1 c2 (lft2rgt,cl) gl =
    let impl2 = mkProd (Anonymous, hyp1, lift 1 hyp2) in
     let th' = mkApp ((Lazy.force coq_proj2), [|impl1; impl2; th|]) in
      Tactics.refine
-      (mkApp (th', [| mkCast (mkMeta (Clenv.new_meta()), hyp1) |])) gl
+      (mkApp (th', [| mkCast (Evarutil.mk_new_meta(), hyp1) |])) gl
 
 let general_s_rewrite lft2rgt c gl =
  let ctype = pf_type_of gl c in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 57804f23aa..e6b2f76ecf 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -40,6 +40,7 @@ open Nametab
 open Genarg
 open Tacexpr
 open Decl_kinds
+open Evarutil
 
 exception Bound
 
@@ -421,7 +422,7 @@ let rec intros_rmove = function
  *  of the type of a term. *)
 
 let apply_type hdcty argl gl =
-  refine (applist (mkCast (mkMeta (new_meta()),hdcty),argl)) gl
+  refine (applist (mkCast (Evarutil.mk_new_meta(),hdcty),argl)) gl
     
 let apply_term hdc argl gl =
   refine (applist (hdc,argl)) gl
@@ -431,17 +432,12 @@ let bring_hyps hyps =
   else
     (fun gl ->
       let newcl = List.fold_right mkNamedProd_or_LetIn hyps (pf_concl gl) in
-      let f = mkCast (mkMeta (new_meta()),newcl) in
+      let f = mkCast (Evarutil.mk_new_meta(),newcl) in
       refine_no_check (mkApp (f, instance_from_named_context hyps)) gl)
 
 (* Resolution with missing arguments *)
 
 let apply_with_bindings (c,lbind) gl = 
-  let apply = 
-    match kind_of_term c with 
-      | Lambda _ -> Clenvtac.res_pf_cast 
-      | _ -> Clenvtac.res_pf 
-  in 
   (* 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. *)
@@ -451,7 +447,7 @@ let apply_with_bindings (c,lbind) gl =
       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 gl n (c,thm_ty) lbind in
-      apply clause gl
+      Clenvtac.res_pf clause gl
     with (Pretype_errors.PretypeError _|RefinerError _|UserError _|Failure _) as exn ->
       let red_thm =
         try red_product (pf_env gl) (project gl) thm_ty
@@ -462,7 +458,7 @@ let apply_with_bindings (c,lbind) gl =
     (* Last chance: if the head is a variable, apply may try
        second order unification *)
     let clause = make_clenv_binding_apply gl (-1) (c,thm_ty0) lbind in 
-    apply clause gl
+    Clenvtac.res_pf clause gl
 
 let apply c = apply_with_bindings (c,NoBindings)
 
@@ -838,7 +834,7 @@ let new_hyp mopt (c,lbind) g =
 	      | Some m -> if m < nargs then list_firstn m tstack else tstack
 	      | None   -> tstack)
   in 
-  (tclTHENLAST (tclTHEN (tclEVARS clause.hook.sigma)
+  (tclTHENLAST (tclTHEN (tclEVARS (evars_of clause.env))
                (cut (pf_type_of g cut_pf)))
      ((tclORELSE (apply cut_pf) (exact_no_check cut_pf)))) g
 
@@ -905,7 +901,7 @@ let elimination_clause_scheme elimclause indclause allow_K gl =
              (str "The type of elimination clause is not well-formed")) 
   in
   let elimclause' = clenv_fchain indmv elimclause indclause in 
-  elim_res_pf elimclause' allow_K gl
+  res_pf elimclause' ~allow_K:allow_K gl
 
 (* cast added otherwise tactics Case (n1,n2) generates (?f x y) and 
  * refine fails *)
@@ -986,7 +982,7 @@ let elimination_in_clause_scheme id elimclause indclause gl =
     errorlabstrm "general_rewrite_in" 
       (str "Nothing to rewrite in " ++ pr_id id);
   tclTHEN
-    (tclEVARS elimclause''.hook.sigma)
+    (tclEVARS (evars_of elimclause''.env))
     (tclTHENS
       (cut new_hyp_typ)
       [ (* Try to insert the new hyp at the same place *)
@@ -1667,7 +1663,7 @@ let elim_scheme_type elim t gl =
         let clause' =
 	  (* t is inductive, then CUMUL or CONV is irrelevant *)
 	  clenv_unify true CUMUL t (clenv_meta_type clause mv) clause in
-	elim_res_pf clause' true gl
+	res_pf clause' ~allow_K:true gl
     | _ -> anomaly "elim_scheme_type"
 
 let elim_type t gl =
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index d2a16dc8eb..cbc690c92c 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -164,8 +164,8 @@ val cut_and_apply         : constr -> tactic
 
 (*s Elimination tactics. *)
 
-val general_elim  : constr with_bindings -> constr with_bindings -> 
-  ?allow_K:bool -> tactic
+val general_elim  :
+  constr with_bindings -> constr with_bindings -> ?allow_K:bool -> tactic
 val default_elim  : constr with_bindings -> tactic
 val simplest_elim : constr -> tactic
 val elim          : constr with_bindings -> constr with_bindings option -> tactic