deuxieme vague de modifs: evar_defs fonctionnel

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

7 files changed, 45 insertions, 58 deletions

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index fc9bd3aa2c..700c8fed7c 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -41,10 +41,9 @@ let e_assumption gl =
   tclFIRST (List.map assumption (pf_ids_of_hyps gl)) gl
 
 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 
-  Clenvtac.e_res_pf kONT clause 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 
+  Clenvtac.e_res_pf clause gl
 
 let e_resolve_constr c gls = e_resolve_with_bindings_tac (c,NoBindings) gls
 			     
diff --git a/tactics/equality.ml b/tactics/equality.ml
index bfedc82204..38dc8f58e4 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -567,10 +567,10 @@ let minimal_free_rels env sigma (c,cty) =
 
 let sig_clausal_form env sigma sort_of_ty siglen ty (dFLT,dFLTty) =
   let { intro = exist_term } = find_sigma_data sort_of_ty in 
-  let isevars = Evarutil.create_evar_defs sigma in
+  let isevars = ref (Evarutil.create_evar_defs sigma) in
   let rec sigrec_clausal_form siglen p_i =
     if siglen = 0 then
-      if Evarconv.the_conv_x env isevars p_i dFLTty then
+      if Evarconv.e_conv env isevars p_i dFLTty then
 	(* the_conv_x had a side-effect on isevars *)
 	dFLT
       else
@@ -579,19 +579,19 @@ let sig_clausal_form env sigma sort_of_ty siglen ty (dFLT,dFLTty) =
       let (a,p_i_minus_1) = match whd_beta_stack p_i with
 	| (_sigS,[a;p]) -> (a,p)
  	| _ -> anomaly "sig_clausal_form: should be a sigma type" in
-      let ev = Evarutil.new_isevar isevars env (dummy_loc,InternalHole)
+      let ev = Evarutil.e_new_isevar isevars env (dummy_loc,InternalHole)
 	(Evarutil.new_Type ()) in
       let rty = beta_applist(p_i_minus_1,[ev]) in
       let tuple_tail = sigrec_clausal_form (siglen-1) rty in
       match
-	Evd.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])
 	| None -> anomaly "Not enough components to build the dependent tuple"
   in
   let scf = sigrec_clausal_form siglen ty in
-  Evarutil.nf_evar (Evarutil.evars_of isevars) scf
+  Evarutil.nf_evar (Evarutil.evars_of !isevars) scf
 
 (* The problem is to build a destructor (a generalization of the
    predecessor) which, when applied to a term made of constructors
diff --git a/tactics/inv.ml b/tactics/inv.ml
index e74fc05a90..7c4456b3d8 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -445,9 +445,8 @@ let rewrite_equations_tac (gene, othin) id neqns names ba =
 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 (wc,kONT) = startWalk gl in
   let t = strong_prodspine (pf_whd_betadeltaiota gl) (pf_type_of gl c) in
-  let indclause = mk_clenv_from wc (c,t) in
+  let indclause = mk_clenv_from (rc_of_glsigma 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 95546142f6..1184815479 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -287,10 +287,9 @@ let add_inversion_lemma_exn na com comsort bool tac =
 
 let lemInv id c gls =
   try
-    let (wc,kONT) = startWalk gls in
-    let clause = mk_clenv_type_of wc c in
+    let clause = mk_clenv_type_of (rc_of_glsigma gls) c in
     let clause = clenv_constrain_with_bindings [(-1,mkVar id)] clause in
-    Clenvtac.elim_res_pf kONT clause true gls
+    Clenvtac.elim_res_pf clause true gls
   with 
     |  UserError (a,b) -> 
 	 errorlabstrm "LemInv" 
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index b8b0cf9aca..195ba3c61b 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -886,10 +886,10 @@ let relation_rewrite c1 c2 (lft2rgt,cl) gl =
      *)
 
 let general_s_rewrite lft2rgt c gl =
- let (wc,_)  = Evar_refiner.startWalk gl in
  let ctype = pf_type_of gl c in
  let eqclause  =
-  Clenv.make_clenv_binding wc (c,ctype) Rawterm.NoBindings in
+  Clenv.make_clenv_binding
+    (Evar_refiner.rc_of_glsigma 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 0e10a0b5d3..72ec0bd2e2 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -324,10 +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 (wc,kONT)  = startWalk gl in
-  let indclause  = mk_clenv_from wc (c,t) in
+  let indclause  = mk_clenv_from (rc_of_glsigma gl) (c,t) in
   let indclause' = clenv_constrain_with_bindings indbindings indclause in
-  let elimclause = mk_clenv_from () (elim,w_type_of wc elim) in
+  let elimclause = mk_clenv_from () (elim,pf_type_of gl elim) in
   let indmv = 
     match kind_of_term (last_arg elimclause.templval.Evd.rebus) with
       | Meta mv -> mv
@@ -371,7 +370,7 @@ let general_elim_then_using
        | None   -> elimclause'
        | Some p -> clenv_assign pmv p elimclause'
   in 
-  elim_res_pf_THEN_i kONT elimclause' branchtacs gl
+  elim_res_pf_THEN_i elimclause' branchtacs gl
 
 
 let elimination_then_using tac predicate (indbindings,elimbindings) c gl = 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d5d972111c..6fe3d75af4 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -442,20 +442,20 @@ let apply_with_bindings (c,lbind) gl =
       | 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
   goal. If this fails, then the head constant will be unfolded step by
   step. *)
-  let thm_ty0 = nf_betaiota (w_type_of wc c) in
+  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
-      apply kONT clause gl
+      apply clause gl
     with (Pretype_errors.PretypeError _|RefinerError _|UserError _|Failure _) as exn ->
       let red_thm =
-        try red_product (w_env wc) (w_Underlying wc) thm_ty
+        try red_product (pf_env gl) (project gl) thm_ty
         with (Redelimination | UserError _) -> raise exn in
       try_apply red_thm in
   try try_apply thm_ty0
@@ -463,7 +463,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 wc (-1) (c,thm_ty0) lbind in 
-    apply kONT clause gl
+    apply clause gl
 
 let apply c = apply_with_bindings (c,NoBindings)
 
@@ -474,9 +474,8 @@ let apply_list = function
 (* Resolution with no reduction on the type *)
 
 let apply_without_reduce c gl = 
-  let (wc,kONT) = startWalk gl in
-  let clause = mk_clenv_type_of wc c in 
-  res_pf kONT clause gl
+  let clause = mk_clenv_type_of (rc_of_glsigma gl) c in 
+  res_pf clause gl
 
 (* A useful resolution tactic which, if c:A->B, transforms |- C into
    |- B -> C and |- A
@@ -831,8 +830,8 @@ let rec intros_clearing = function
 (* Adding new hypotheses  *)
 
 let new_hyp mopt (c,lbind) g =
-  let (wc,kONT) = startWalk g in
-  let clause  = make_clenv_binding wc (c,w_type_of wc c) lbind in
+  let clause  =
+    make_clenv_binding (rc_of_glsigma 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 = 
@@ -841,7 +840,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 (kONT clause.hook)
+  (tclTHENLAST (tclTHEN (tclEVARS clause.hook.sigma)
                (cut (pf_type_of g cut_pf)))
      ((tclORELSE (apply cut_pf) (exact_no_check cut_pf)))) g
 
@@ -896,19 +895,11 @@ let simplest_split = split NoBindings
 (*       Elimination tactics                *)
 (********************************************)
 
-
-(* kONT : ??
- * wc : ??
- * elimclause : ??
- * inclause : ??
- * gl : the current goal
-*)
-
 let last_arg c = match kind_of_term c with
   | App (f,cl) ->  array_last cl
   | _ -> anomaly "last_arg"
 	
-let elimination_clause_scheme kONT elimclause indclause allow_K gl = 
+let elimination_clause_scheme elimclause indclause allow_K gl = 
   let indmv = 
     (match kind_of_term (last_arg (clenv_template elimclause).rebus) with
        | Meta mv -> mv
@@ -916,7 +907,7 @@ let elimination_clause_scheme kONT 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 kONT elimclause' allow_K gl
+  elim_res_pf elimclause' allow_K gl
 
 (* cast added otherwise tactics Case (n1,n2) generates (?f x y) and 
  * refine fails *)
@@ -933,13 +924,13 @@ let type_clenv_binding wc (c,t) lbind =
  *)
 
 let general_elim (c,lbindc) (elimc,lbindelimc) ?(allow_K=true) gl = 
-  let (wc,kONT)  = startWalk gl in
   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 wc (c,t) lbindc  in
-  let elimt      = w_type_of wc elimc in
-  let elimclause = make_clenv_binding wc (elimc,elimt) lbindelimc in 
-  elimination_clause_scheme kONT elimclause indclause allow_K gl
+  let indclause  = make_clenv_binding (rc_of_glsigma 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 
+  elimination_clause_scheme elimclause indclause allow_K gl
 
 (* Elimination tactic with bindings but using the default elimination 
  * constant associated with the type. *)
@@ -980,7 +971,7 @@ let simplest_elim c = default_elim (c,NoBindings)
 
 (* Elimination in hypothesis *)
 
-let elimination_in_clause_scheme kONT id elimclause indclause =
+let elimination_in_clause_scheme id elimclause indclause =
   let (hypmv,indmv) = 
     match clenv_independent elimclause with
         [k1;k2] -> (k1,k2)
@@ -998,7 +989,7 @@ let elimination_in_clause_scheme kONT id elimclause indclause =
     errorlabstrm "general_rewrite_in" 
       (str "Nothing to rewrite in " ++ pr_id id);
   tclTHEN
-    (kONT elimclause''.hook)
+    (tclEVARS elimclause''.hook.sigma)
     (tclTHENS
       (cut new_hyp_typ)
       [ (* Try to insert the new hyp at the same place *)
@@ -1007,13 +998,14 @@ let elimination_in_clause_scheme kONT id elimclause indclause =
         refine_no_check new_hyp_prf])
 
 let general_elim_in id (c,lbindc) (elimc,lbindelimc) gl = 
-  let (wc,kONT)  = startWalk gl in
   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 wc (c,t) lbindc  in
-  let elimt      = w_type_of wc elimc in
-  let elimclause = make_clenv_binding wc (elimc,elimt) lbindelimc in 
-  elimination_in_clause_scheme kONT id elimclause indclause gl
+  let indclause  =
+    make_clenv_binding (rc_of_glsigma 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 
+  elimination_in_clause_scheme id elimclause indclause gl
 
 (* Case analysis tactics *)
 
@@ -1384,11 +1376,11 @@ let cook_sign hyp0 indvars env =
 
 let induction_tac varname typ ((elimc,lbindelimc),elimt) gl =
   let c = mkVar varname in
-  let (wc,kONT)  = startWalk gl                    in
+  let wc = rc_of_glsigma gl in
   let indclause  = make_clenv_binding wc (c,typ) NoBindings  in
   let elimclause =
     make_clenv_binding wc (mkCast (elimc,elimt),elimt) lbindelimc in
-  elimination_clause_scheme kONT elimclause indclause true gl
+  elimination_clause_scheme elimclause indclause true gl
 
 let make_up_names7 n ind (old_style,cname) = 
   if old_style (* = V6.3 version of Induction on hypotheses *)
@@ -1675,14 +1667,13 @@ let simple_destruct = function
  *)
 
 let elim_scheme_type elim t gl =
-  let (wc,kONT) = startWalk gl in
-  let clause = mk_clenv_type_of wc elim in 
+  let clause = mk_clenv_type_of (rc_of_glsigma gl) elim in
   match kind_of_term (last_arg (clenv_template clause).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
-	elim_res_pf kONT clause' true gl
+	elim_res_pf clause' true gl
     | _ -> anomaly "elim_scheme_type"
 
 let elim_type t gl =