From e0c40f091cecd6335ce41a2b904db326996863a2 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Thu, 7 Nov 2013 17:05:26 +0000
Subject: Partial application hunt.

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

(limited to 'pretyping')

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 6510655b99..8d2234022b 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -579,12 +579,12 @@ let dependent_main noevar 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)
+	    CArray.Fun1.iter deprec m
 	      (Array.sub lt
 		(Array.length lm) ((Array.length lt) - (Array.length lm)))
 	| _, Cast (c,_,_) when noevar && isMeta c -> ()
 	| _, Evar _ when noevar -> ()
-	| _ -> iter_constr_with_binders (lift 1) deprec m t
+	| _ -> iter_constr_with_binders (fun c -> lift 1 c) deprec m t
   in
   try deprec m t; false with Occur -> true
 
-- 
cgit v1.2.3