Plus de whd_castapp_stack

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

2 files changed, 13 insertions, 8 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 7fb05a144c..7271103bcc 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -676,10 +676,14 @@ let constrain_clenv_to_subterm clause (op,cl) =
        then clenv_unify op cl clause,cl
        else error "Bound 1"
      with ex when catchable_exception ex ->
-       (match kind_of_term (telescope_appl cl) with 
-	  | IsAppL (c1,[|c2|]) ->
+       (match kind_of_term cl with 
+	  | IsAppL (f,args) ->
+	      let n = Array.length args in
+	      assert (n>0);
+	      let c1 = mkAppL (f,Array.sub args 0 (n-1)) in
+	      let c2 = args.(n-1) in
 	      (try 
-		 matchrec c1 
+		 matchrec c1
 	       with ex when catchable_exception ex -> 
 		 matchrec c2)
           | IsProd (_,t,c) ->
@@ -929,7 +933,7 @@ let secondOrderAbstraction allow_K gl p oplist clause =
     clause'
 
 let clenv_so_resolver allow_K clause gl =
-  let c, oplist = whd_castapp_stack (clenv_instance_template_type clause) [] in
+  let c, oplist = whd_stack (clenv_instance_template_type clause) in
   match kind_of_term c with
     | IsMeta p ->
 	let clause' = secondOrderAbstraction allow_K gl p oplist clause in 
@@ -948,8 +952,8 @@ let clenv_so_resolver allow_K clause gl =
    Meta(1) had meta-variables in it. *)
 
 let clenv_unique_resolver allow_K clenv gls =
-  let pathd,_ = whd_castapp_stack (clenv_instance_template_type clenv) [] in
-  let glhd,_ = whd_castapp_stack (pf_concl gls) [] in
+  let pathd,_ = whd_stack (clenv_instance_template_type clenv) in
+  let glhd,_ = whd_stack (pf_concl gls)in
   match kind_of_term pathd, kind_of_term glhd with
     | IsMeta _, IsLambda _ ->
 	(try 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6c4665fd35..3f864682e4 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -814,7 +814,7 @@ let new_hyp mopt c blist g =
   let (wc,kONT) = startWalk g in
   let clause  = mk_clenv_printable_type_of wc c in
   let clause' = clenv_match_args blist clause in
-  let (thd,tstack) = whd_castapp_stack (clenv_instance_template clause')[] in
+  let (thd,tstack) = whd_stack (clenv_instance_template clause') in
   let nargs = List.length tstack in
   let cut_pf = 
     applist(thd, 
@@ -1089,7 +1089,8 @@ let atomize_param_of_ind hyp0 gl =
     if i<>nparams then 
       let tmptyp0 = pf_get_hyp_typ gl hyp0 in
       let (_,indtyp,_) = pf_reduce_to_mind gl tmptyp0 in
-      match kind_of_term (destAppL (whd_castapp indtyp)).(i) with
+      let argl = snd (decomp_app indtyp) in
+      match kind_of_term (List.index argl (i-1)) with
 	| IsVar id when not (List.exists (occur_var id) avoid) ->
 	    atomize_one (i-1) ((mkVar id)::avoid) gl
 	| IsVar id ->