Suppression du retypage dans w_Declare

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

3 files changed, 7 insertions, 11 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 94d3c1b69..bdd1a8ba1 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -67,12 +67,11 @@ let applyHead n c wc =
     else 
       match kind_of_term (w_whd_betadeltaiota wc cty) with
         | IsProd (_,c1,c2) ->
-            let c1ty = w_type_of wc c1 in
 	    let evar = Evarutil.new_evar_in_sign (w_env wc) in
             let (evar_n, _) = destEvar evar in
 	    (compose 
 	       (apprec (n-1) (applist(c,[evar])) (subst1 evar c2))
-	       (w_Declare evar_n (c1,c1ty)))
+	       (w_Declare evar_n c1))
 	    wc
 	| _ -> error "Apply_Head_Then"
   in 
@@ -946,9 +945,7 @@ let clenv_pose_dependent_evars clenv =
        let evar = Evarutil.new_evar_in_sign (w_env clenv.hook) in
        let (evar_n,_) = destEvar evar in
        let tY = clenv_instance_type clenv mv in
-       let tYty = w_type_of clenv.hook tY in
-       let clenv' = clenv_wtactic (w_Declare evar_n (tY,tYty))
-		      clenv in
+       let clenv' = clenv_wtactic (w_Declare evar_n tY) clenv in
        clenv_assign mv evar clenv')
     clenv
     dep_mvs
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index f99608691..9e9d6c8fb 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -133,12 +133,11 @@ let w_whd_betadeltaiota wc c = whd_betadeltaiota (w_env wc) (w_Underlying wc) c
 let w_hnf_constr wc c        = hnf_constr (w_env wc) (w_Underlying wc) c
 
 
-let w_Declare sp (ty,s) (wc : walking_constraints) =
-  let c = mkCast (ty,s) in
-  let _ = w_type_of wc c in
+let w_Declare sp ty (wc : walking_constraints) =
+  let _ = w_type_of wc ty in (* Utile ?? *)
   let access  = get_focus (ids_it wc)
   and sign = get_hyps (ids_it wc) in
-  let newdecl = mk_goal (mt_ctxt access) sign c in 
+  let newdecl = mk_goal (mt_ctxt access) sign ty in 
   ((ids_mod (fun evc -> (rc_add evc (sp,newdecl))) wc): walking_constraints)
 
 let w_Declare_At sp sp' c = w_Focusing sp (w_Declare sp' c)
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index b5af7f131..88071b3af 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -52,8 +52,8 @@ val walking         : w_tactic -> tactic
 val w_Focusing_THEN : 
   evar -> 'a result_w_tactic -> ('a -> w_tactic) -> w_tactic
 
-val w_Declare    : evar -> constr * constr -> w_tactic
-val w_Declare_At : evar -> evar -> constr * constr -> w_tactic
+val w_Declare    : evar -> types -> w_tactic
+val w_Declare_At : evar -> evar -> types -> w_tactic
 val w_Define     : evar -> constr -> w_tactic
 
 val w_Underlying : walking_constraints -> enamed_declarations