From 88095bc8eebfeabf0f3a5dee981091aa12002b05 Mon Sep 17 00:00:00 2001
From: jforest
Date: Mon, 1 Mar 2010 13:59:34 +0000
Subject: amelioration mineure dans Function

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12826 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/funind/rawterm_to_relation.ml | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/funind/rawterm_to_relation.ml b/plugins/funind/rawterm_to_relation.ml
index f69dd2fe68..3c3a36f037 100644
--- a/plugins/funind/rawterm_to_relation.ml
+++ b/plugins/funind/rawterm_to_relation.ml
@@ -500,6 +500,18 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 	in
 	begin
 	  match f with
+	    | RLambda _  -> 
+		let rec aux t l = 
+		  match l with 
+		    | [] -> t
+		    | u::l -> 
+			match t with 
+			  | RLambda(loc,na,_,nat,b) -> 
+			      RLetIn(dummy_loc,na,u,aux b l)
+			  | _ -> 
+			      RApp(dummy_loc,t,l)
+		in
+		build_entry_lc env funnames avoid (aux f args)
 	    | RVar(_,id) when Idset.mem id funnames ->
 		(* if we have [f t1 ... tn] with [f]$\in$[fnames]
 		   then we create a fresh variable [res],
@@ -566,7 +578,7 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 		  funnames
 		  avoid
 		  (mkRLetIn(new_n,t,mkRApp(new_b,args)))
-	    | RCases _ | RLambda _ | RIf _ | RLetTuple _ ->
+	    | RCases _  | RIf _ | RLetTuple _ ->
 		(* we have [(match e1, ...., en with ..... end) t1 tn]
 		   we first compute the result from the case and
 		   then combine each of them with each of args one
-- 
cgit v1.2.3