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

4 files changed, 31 insertions, 40 deletions

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 3d2e3fde0d..e594f9a9df 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -693,16 +693,6 @@ type constr_pattern_expr = constr_expr
 
 let default_binder_kind = Default Explicit
 
-let rec local_binders_length = function
-  | [] -> 0
-  | LocalRawDef _::bl -> 1 + local_binders_length bl
-  | LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl
-
-let rec local_assums_length = function
-  | [] -> 0
-  | LocalRawDef _::bl -> local_binders_length bl
-  | LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl
-
 let names_of_local_assums bl =
   List.flatten (List.map (function LocalRawAssum(l,_,_)->l|_->[]) bl)
 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 36f8cfad39..6e3951b2fa 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -216,12 +216,6 @@ val mkCProdN : loc -> local_binder list -> constr_expr -> constr_expr
 
 (* For binders parsing *)
 
-(* Includes let binders *)
-val local_binders_length : local_binder list -> int
-
-(* Excludes let binders *)
-val local_assums_length : local_binder list -> int
-
 (* With let binders *)
 val names_of_local_binders : local_binder list -> name located list
 
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')
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 50cc702e21..75f0daa7f8 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -59,43 +59,43 @@ let rec complete_conclusion a cs = function
 
 (* 1| Constant definitions *)
 
-let red_constant_entry bl ce = function
+let red_constant_entry n ce = function
   | None -> ce
   | Some red ->
       let body = ce.const_entry_body in
       { ce with const_entry_body =
-	under_binders (Global.env()) (fst (reduction_of_red_expr red))
-	  (local_binders_length bl)
-	  body }
+	under_binders (Global.env()) (fst (reduction_of_red_expr red)) n body }
 
 let interp_definition boxed bl red_option c ctypopt =
   let env = Global.env() in
+  let evdref = ref Evd.empty in
+  let (env_bl, ctx), imps1 =
+    interp_context_evars ~fail_anonymous:false evdref env bl in
   let imps,ce =
     match ctypopt with
       None ->
-	let b = abstract_constr_expr c bl in
-	let b, imps = interp_constr_evars_impls env b in
-	  imps,
-	{ const_entry_body = b;
+	let c, imps2 = interp_constr_evars_impls ~evdref ~fail_evar:false env_bl c in
+	let body = nf_isevar !evdref (it_mkLambda_or_LetIn c ctx) in
+	check_evars env Evd.empty !evdref body;
+	imps1@imps2,
+	{ const_entry_body = body;
 	  const_entry_type = None;
           const_entry_opaque = false;
 	  const_entry_boxed = boxed }
     | Some ctyp ->
-	let ty = prod_constr_expr ctyp bl in
-	let b = abstract_constr_expr c bl in
-	let evdref = ref Evd.empty in
-	let ty, impls = interp_type_evars_impls ~evdref ~fail_evar:false env ty in
-	let b, imps = interp_casted_constr_evars_impls ~evdref ~fail_evar:false env b ty in
-	let body, typ = nf_isevar !evdref b, nf_isevar !evdref ty in
-	  check_evars env Evd.empty !evdref body;
-	  check_evars env Evd.empty !evdref typ;
-	  imps,
+	let ty, impls = interp_type_evars_impls ~evdref ~fail_evar:false env_bl ctyp in
+	let c, imps2 = interp_casted_constr_evars_impls ~evdref ~fail_evar:false env_bl c ty in
+	let body = nf_isevar !evdref (it_mkLambda_or_LetIn c ctx) in
+	let typ = nf_isevar !evdref (it_mkProd_or_LetIn ty ctx) in
+	check_evars env Evd.empty !evdref body;
+	check_evars env Evd.empty !evdref typ;
+	imps1@imps2,
 	{ const_entry_body = body;
 	  const_entry_type = Some typ;
           const_entry_opaque = false;
 	  const_entry_boxed = boxed }
   in
-  red_constant_entry bl ce red_option, imps
+  red_constant_entry (rel_context_length ctx) ce red_option, imps
 
 let declare_global_definition ident ce local k imps =
   let kn = declare_constant ident (DefinitionEntry ce,IsDefinition k) in
@@ -484,8 +484,8 @@ let prepare_recursive_declaration fixnames fixtypes fixdefs =
 
 (* Jump over let-bindings. *)
 
-let compute_possible_guardness_evidences n fix =
-  match index_of_annot fix.fix_binders n with
+let compute_possible_guardness_evidences na fix (nb,_) =
+  match index_of_annot fix.fix_binders na with
   | Some i -> [i]
   | None ->
       (* If recursive argument was not given by user, we try all args.
@@ -493,7 +493,7 @@ let compute_possible_guardness_evidences n fix =
 	 but doing it properly involves delta-reduction, and it finally
          doesn't seem to worth the effort (except for huge mutual
 	 fixpoints ?) *)
-      interval 0 (local_assums_length fix.fix_binders - 1)
+      interval 0 (nb - 1)
 
 type recursive_preentry =
   identifier list * constr option list * types list
@@ -608,9 +608,10 @@ let extract_cofixpoint_components l =
 
 let do_fixpoint l b =
   let fixl,ntns,wfl = extract_fixpoint_components l in
+  let fix = interp_fixpoint fixl ntns in
   let possible_indexes =
-      List.map2 compute_possible_guardness_evidences wfl fixl in
-  declare_fixpoint b (interp_fixpoint fixl ntns) possible_indexes ntns
+    list_map3 compute_possible_guardness_evidences wfl fixl (snd fix) in
+  declare_fixpoint b fix possible_indexes ntns
 
 let do_cofixpoint l b =
   let fixl,ntns = extract_cofixpoint_components l in