From cd21a1067dcf4506a69f86c42a593c21dca5abd5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 23 Dec 2002 22:01:09 +0000
Subject: Prise en compte application partielle dans dependent

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3478 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/termops.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index c936987839..b233ce2441 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -386,7 +386,13 @@ let dependent m t =
     if eq_constr m t then
       raise Occur
     else
-      iter_constr_with_binders (lift 1) deprec m t
+      match kind_of_term m, kind_of_term t with
+	| App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
+	    deprec m (mkApp (ft,Array.sub lt 0 (Array.length lm)));
+	    Array.iter (deprec m)
+	      (Array.sub lt 
+		(Array.length lm) ((Array.length lt) - (Array.length lm)))
+	| _ -> iter_constr_with_binders (lift 1) deprec m t
   in 
   try deprec m t; false with Occur -> true
 
-- 
cgit v1.2.3