simplification de clenv

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

6 files changed, 27 insertions, 27 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 0dc0a9f4c..66454059e 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -44,10 +44,10 @@ open Tacexpr
 (****************************************************************************)
 
 type auto_tactic = 
-  | Res_pf     of constr * wc clausenv (* Hint Apply *)
-  | ERes_pf    of constr * wc clausenv (* Hint EApply *)
+  | Res_pf     of constr * clausenv (* Hint Apply *)
+  | ERes_pf    of constr * clausenv (* Hint EApply *)
   | Give_exact of constr                  
-  | Res_pf_THEN_trivial_fail of constr * wc clausenv (* Hint Immediate *)
+  | Res_pf_THEN_trivial_fail of constr * clausenv (* Hint Immediate *)
   | Unfold_nth of global_reference       (* Hint Unfold *)
   | Extern     of glob_tactic_expr       (* Hint Extern *) 
 
@@ -195,7 +195,7 @@ let make_apply_entry env sigma (eapply,verbose) name (c,cty) =
   match kind_of_term cty with
     | Prod _ ->
         let ce = mk_clenv_from dummy_goal (c,cty) in
-	let c' = (clenv_template_type ce).rebus in
+	let c' = clenv_type ce in
 	let pat = Pattern.pattern_of_constr c' in
         let hd = (try head_pattern_bound pat
                   with BoundPattern -> failwith "make_apply_entry") in
@@ -263,7 +263,7 @@ let make_trivial env sigma (name,c) =
   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);
+               pat = Some (Pattern.pattern_of_constr (clenv_type ce));
                code=Res_pf_THEN_trivial_fail(c,ce) })
 
 open Vernacexpr
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 18daa6ebe..950e272bc 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -24,10 +24,10 @@ open Vernacexpr
 (*i*)
   
 type auto_tactic = 
-  | Res_pf     of constr * wc clausenv    (* Hint Apply *)
-  | ERes_pf    of constr * wc clausenv    (* Hint EApply *)
+  | Res_pf     of constr * clausenv    (* Hint Apply *)
+  | ERes_pf    of constr * clausenv    (* Hint EApply *)
   | Give_exact of constr                  
-  | Res_pf_THEN_trivial_fail of constr * wc clausenv (* Hint Immediate *)
+  | Res_pf_THEN_trivial_fail of constr * 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 * wc clausenv) -> tactic
+val unify_resolve : (constr * clausenv) -> tactic
 
 (* [ConclPattern concl pat tacast]:
    if the term concl matches the pattern pat, (in sense of 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 9a02ba608..0ac120327 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -448,8 +448,8 @@ let raw_inversion inv_kind indbinding id status names gl =
   let t = strong_prodspine (pf_whd_betadeltaiota gl) (pf_type_of gl c) 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
+  let newc = clenv_value indclause' in
+  let ccl = clenv_type indclause' in
   check_no_metas indclause' ccl;
   let IndType (indf,realargs) =
     try find_rectype env sigma ccl
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 7961a7dc9..905ca60b4 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -961,9 +961,9 @@ let relation_rewrite c1 c2 (lft2rgt,cl) gl =
      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
+   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
  in
   let input_relation = relation_of_hypothesis_and_term_to_rewrite gl hyp c1 in
   let marked_but = mark_occur c1 but in
@@ -979,8 +979,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 gl (c,ctype) Rawterm.NoBindings in
- let (equiv, args) =
-  decompose_app (Clenv.clenv_instance_template_type eqclause) in
+ let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
  let rec get_last_two = function
    | [c1;c2] -> (c1, c2)
    | x::y::z -> get_last_two (y::z)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index fa5eeaef3..79aa71c0f 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -359,8 +359,8 @@ let general_elim_then_using
                    0 branchsigns.(i);
                branchnum = i+1;
                ity = ity;
-               largs = List.map (clenv_instance_term ce) largs;
-               pred = clenv_instance_term ce hd }
+               largs = List.map (clenv_nf_meta ce) largs;
+               pred = clenv_nf_meta ce hd }
     in 
     tac ba gl
   in
@@ -368,7 +368,8 @@ let general_elim_then_using
   let elimclause' =
     match predicate with
        | None   -> elimclause'
-       | Some p -> clenv_assign pmv p elimclause'
+       | Some p ->
+           clenv_unify true Reductionops.CONV (mkMeta pmv) p elimclause'
   in 
   elim_res_pf_THEN_i elimclause' branchtacs gl
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d64c90916..57804f23a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -830,7 +830,7 @@ let rec intros_clearing = function
 
 let new_hyp mopt (c,lbind) g =
   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 (thd,tstack) = whd_stack (clenv_value clause) in
   let nargs = List.length tstack in
   let cut_pf = 
     applist(thd, 
@@ -899,7 +899,7 @@ let last_arg c = match kind_of_term c with
 	
 let elimination_clause_scheme elimclause indclause allow_K gl = 
   let indmv = 
-    (match kind_of_term (last_arg (clenv_template elimclause).rebus) with
+    (match kind_of_term (last_arg elimclause.templval.rebus) with
        | Meta mv -> mv
        | _  -> errorlabstrm "elimination_clause"
              (str "The type of elimination clause is not well-formed")) 
@@ -911,7 +911,7 @@ let elimination_clause_scheme elimclause indclause allow_K gl =
  * refine fails *)
 
 let type_clenv_binding wc (c,t) lbind = 
-  clenv_instance_template_type (make_clenv_binding wc (c,t) lbind)
+  clenv_type (make_clenv_binding wc (c,t) lbind)
 
 (* 
  * Elimination tactic with bindings and using an arbitrary 
@@ -976,12 +976,12 @@ let elimination_in_clause_scheme id elimclause indclause gl =
           (str "The type of elimination clause is not well-formed") in
   let elimclause'  = clenv_fchain indmv elimclause indclause in 
   let hyp = mkVar id in
-  let hyp_typ = clenv_type_of elimclause' hyp in
+  let hyp_typ = pf_type_of gl hyp in
   let hypclause =
     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
+  let new_hyp_prf  = clenv_value elimclause'' in
+  let new_hyp_typ  = clenv_type elimclause'' in
   if eq_constr hyp_typ new_hyp_typ then
     errorlabstrm "general_rewrite_in" 
       (str "Nothing to rewrite in " ++ pr_id id);
@@ -1662,11 +1662,11 @@ let simple_destruct = function
 
 let elim_scheme_type elim t gl =
   let clause = mk_clenv_type_of gl elim in
-  match kind_of_term (last_arg (clenv_template clause).rebus) with
+  match kind_of_term (last_arg clause.templval.rebus) with
     | Meta mv ->
         let clause' =
 	  (* t is inductive, then CUMUL or CONV is irrelevant *)
-	  clenv_unify true CUMUL t (clenv_instance_type clause mv) clause in
+	  clenv_unify true CUMUL t (clenv_meta_type clause mv) clause in
 	elim_res_pf clause' true gl
     | _ -> anomaly "elim_scheme_type"