diff options
| author |  jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-03-01 13:59:34 +0000 |
|---|---|---|
| committer | jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-03-01 13:59:34 +0000 |
| commit | 88095bc8eebfeabf0f3a5dee981091aa12002b05 (patch) | |
| tree | 7bf3a390c14dc95e708b9024cbb561ad59f60a5c /plugins | |
| parent | 7cb299f5c1b534246e92e99b39aa4e2b84fbb9e4 (diff) | |
amelioration mineure dans Function
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12826 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/rawterm_to_relation.ml | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/plugins/funind/rawterm_to_relation.ml b/plugins/funind/rawterm_to_relation.ml index f69dd2fe6..3c3a36f03 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 |