From a69a9d0c3792da57dfbc513d47c2a36dd3328ab3 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 1 Oct 2000 13:36:51 +0000
Subject: Plus de whd_castapp_stack

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@623 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/clenv.ml | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

(limited to 'proofs')

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 
-- 
cgit v1.2.3