From 7cf251501d7cc1567630c947de981fb407a773c4 Mon Sep 17 00:00:00 2001
From: glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 4 Mar 2011 13:07:42 +0000
Subject: checker: add eta-expansion

Backport of changes introduced in r13443 and r13494.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13866 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 checker/closure.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'checker/closure.ml')

diff --git a/checker/closure.ml b/checker/closure.ml
index bd7347134..58c80b521 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -651,6 +651,12 @@ let rec get_args n tys f e stk =
           get_args (n-na) etys f (subs_cons(l,e)) s
     | _ -> (Inr {norm=Cstr;term=FLambda(n,tys,f,e)}, stk)
 
+(* Eta expansion: add a reference to implicit surrounding lambda at end of stack *)
+let rec eta_expand_stack = function
+  | (Zapp _ | Zfix _ | Zcase _ | Zshift _ | Zupdate _ as e) :: s ->
+      e :: eta_expand_stack s
+  | [] ->
+      [Zshift 1; Zapp [|{norm=Norm; term= FRel 1}|]]
 
 (* Iota reduction: extract the arguments to be passed to the Case
    branches *)
-- 
cgit v1.2.3