Fixing #5420 as well as many related bugs due to miscounting let-ins.

- Supporting let-ins in tactic "fix", and hence in interactive
  Fixpoint and mutual theorems.
- Documenting more precisely the meaning of n in tactic "fix id n".
- Fixing computation of recursive index at interpretation time in the
  presence of let-ins.

6 files changed, 23 insertions, 18 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 3f12411863..0edc66f839 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2618,9 +2618,9 @@ as the ones described in Section~\ref{Tac-induction}.
 In the syntax of the tactic, the identifier {\ident} is the name given
 to the induction hypothesis. The natural number {\num} tells on which
 premise of the current goal the induction acts, starting
-from 1 and counting both dependent and non dependent
-products. Especially, the current lemma must be composed of at least
-{\num} products.
+from 1, counting both dependent and non dependent
+products, but skipping local definitions. Especially, the current
+lemma must be composed of at least {\num} products.
 
 Like in a {\tt fix} expression, the induction
 hypotheses have to be used on structurally smaller arguments.
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0aab773140..43fc1d5111 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -507,6 +507,9 @@ let rec check_mutind env sigma k cl = match kind_of_term (strip_outer_cast cl) w
   else
     let open Context.Rel.Declaration in
     check_mutind (push_rel (LocalAssum (na, c1)) env) sigma (pred k) b
+| LetIn (na, c1, t, b) ->
+    let open Context.Rel.Declaration in
+    check_mutind (push_rel (LocalDef (na, c1, t)) env) sigma k b
 | _ -> error "Not enough products."
 
 (* Refine as a fixpoint *)
diff --git a/vernac/command.ml b/vernac/command.ml
index c24dbdf7c0..a6343a5f5d 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -867,8 +867,10 @@ let prepare_recursive_declaration fixnames fixtypes fixdefs =
 
 (* Jump over let-bindings. *)
 
-let compute_possible_guardness_evidences (ids,_,na) =
-  match na with
+let compute_possible_guardness_evidences (ctx,_,recindex) =
+  (* A recursive index is characterized by the number of lambdas to
+     skip before finding the relevant inductive argument *)
+  match recindex with
   | Some i -> [i]
   | None ->
       (* If recursive argument was not given by user, we try all args.
@@ -876,7 +878,7 @@ let compute_possible_guardness_evidences (ids,_,na) =
 	 but doing it properly involves delta-reduction, and it finally
          doesn't seem to worth the effort (except for huge mutual
 	 fixpoints ?) *)
-      List.interval 0 (List.length ids - 1)
+      List.interval 0 (Context.Rel.nhyps ctx - 1)
 
 type recursive_preentry =
   Id.t list * constr option list * types list
@@ -1136,10 +1138,10 @@ let interp_recursive isfix fixl notations =
   let evd, nf = nf_evars_and_universes evd in
   let fixdefs = List.map (Option.map nf) fixdefs in
   let fixtypes = List.map nf fixtypes in
-  let fixctxnames = List.map (fun (_,ctx) -> List.map RelDecl.get_name ctx) fixctxs in
+  let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in
 
   (* Build the fix declaration block *)
-  (env,rec_sign,all_universes,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxnames fiximps fixannots
+  (env,rec_sign,all_universes,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots
 
 let check_recursive isfix env evd (fixnames,fixdefs,_) =
   check_evars_are_solved env evd Evd.empty;
@@ -1162,7 +1164,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
-      List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps))))
+      List.map3 (fun id t (ctx,imps,_) -> ((id,pl),(t,(List.map RelDecl.get_name ctx,imps))))
 		fixnames fixtypes fiximps in
     let init_tac =
       Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
@@ -1199,7 +1201,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
-      List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps))))
+      List.map3 (fun id t (ctx,imps,_) -> ((id,pl),(t,(List.map RelDecl.get_name ctx,imps))))
 		fixnames fixtypes fiximps in
     let init_tac =
       Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
diff --git a/vernac/command.mli b/vernac/command.mli
index bccc22ae92..b62611e2e7 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -138,24 +138,24 @@ type recursive_preentry =
 val interp_fixpoint :
   structured_fixpoint_expr list -> decl_notation list ->
     recursive_preentry * lident list option * Evd.evar_universe_context * 
-    (Name.t list * Impargs.manual_implicits * int option) list
+    (Context.Rel.t * Impargs.manual_implicits * int option) list
 
 val interp_cofixpoint :
   structured_fixpoint_expr list -> decl_notation list ->
     recursive_preentry * lident list option * Evd.evar_universe_context * 
-    (Name.t list * Impargs.manual_implicits * int option) list
+    (Context.Rel.t * Impargs.manual_implicits * int option) list
 
 (** Registering fixpoints and cofixpoints in the environment *)
 
 val declare_fixpoint :
   locality -> polymorphic ->
   recursive_preentry * lident list option * Evd.evar_universe_context * 
-  (Name.t list * Impargs.manual_implicits * int option) list ->
+  (Context.Rel.t * Impargs.manual_implicits * int option) list ->
   lemma_possible_guards -> decl_notation list -> unit
 
 val declare_cofixpoint : locality -> polymorphic -> 
   recursive_preentry * lident list option * Evd.evar_universe_context * 
-  (Name.t list * Impargs.manual_implicits * int option) list ->
+  (Context.Rel.t * Impargs.manual_implicits * int option) list ->
   decl_notation list -> unit
 
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 430d48bc76..ca511b573c 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -100,10 +100,10 @@ let find_mutually_recursive_statements thms =
           match kind_of_term t with
           | Ind ((kn,_ as ind),u) when
                 let mind = Global.lookup_mind kn in
-                mind.mind_finite <> Decl_kinds.CoFinite && is_local_assum decl ->
+                mind.mind_finite <> Decl_kinds.CoFinite ->
               [ind,x,i]
           | _ ->
-              []) 0 (List.rev whnf_hyp_hds)) in
+              []) 0 (List.rev (List.filter RelDecl.is_local_assum whnf_hyp_hds))) in
       let ind_ccl =
         let cclenv = push_rel_context hyps (Global.env()) in
         let whnf_ccl,_ = whd_all_stack cclenv Evd.empty ccl in
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 39c089be9f..6b45ed9339 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -41,8 +41,8 @@ val start_proof_com :
 val start_proof_with_initialization : 
   goal_kind -> Evd.evar_map ->
   (bool * lemma_possible_guards * unit Proofview.tactic list option) option ->
-  ((Id.t * universe_binders option) *
-     (types * (Name.t list * Impargs.manual_explicitation list))) list
+  ((Id.t (* name of thm *) * universe_binders option) *
+     (types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list
   -> int list option -> unit declaration_hook -> unit
 
 val universe_proof_terminator :