diff options
| author | herbelin | 2009-12-12 22:59:29 +0000 |
|---|---|---|
| committer | herbelin | 2009-12-12 22:59:29 +0000 |
| commit | 563d9e1066c7f6f0fb0263101013b015b3faa0bd (patch) | |
| tree | 23d43cbd86999502e1da03bd46ff7d87aafa0ccc /plugins | |
| parent | aba4b1924f562d861ab2cf7ec75c507f0efe0d1f (diff) | |
Fixed incorrect computation of possible guard in presence of `{ ... } contexts.
Also removed used of local_binders_length and local_assums_length
which are now incorrect due to the possible presence of `{ ... } contexts.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12579 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/indfun.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 781a841c95..5ab65583a0 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -235,8 +235,14 @@ let rec is_rec names = in lookup names +let rec local_binders_length = function + (* Assume that no `{ ... } contexts occur *) + | [] -> 0 + | Topconstr.LocalRawDef _::bl -> 1 + local_binders_length bl + | Topconstr.LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl + let prepare_body (name,annot,args,types,body) rt = - let n = (Topconstr.local_binders_length args) in + let n = local_binders_length args in (* Pp.msgnl (str "nb lambda to chop : " ++ str (string_of_int n) ++ fnl () ++Printer.pr_rawconstr rt); *) let fun_args,rt' = chop_rlambda_n n rt in (fun_args,rt') |