From 563d9e1066c7f6f0fb0263101013b015b3faa0bd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 12 Dec 2009 22:59:29 +0000
Subject: 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
---
 plugins/funind/indfun.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'plugins')

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')
-- 
cgit v1.2.3