From 1a43fda0dc9bb8d100808426980446353f8f1ae3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Apr 2017 11:21:23 +0200
Subject: Removing internal support for accepting "{struct x}" and co in
 "Theorem with".

There were actually no syntax for it, and I'm still unsure what good
syntax to give to it, even more that it would be useful to have one.
---
 ide/texmacspp.ml        |  2 +-
 intf/vernacexpr.mli     |  2 +-
 parsing/g_vernac.ml4    |  4 ++--
 printing/ppvernac.ml    |  3 +--
 vernac/lemmas.ml        | 25 ++++---------------------
 vernac/vernacentries.ml |  4 ++--
 6 files changed, 11 insertions(+), 29 deletions(-)

diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index e787e48bf1..74d0438dd4 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -553,7 +553,7 @@ let rec tmpp v loc =
       let str_dk = Kindops.string_of_definition_kind (l, false, dk) in
       let str_id = Id.to_string id in
       (xmlDef str_dk str_id loc [pp_expr e])
-  | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement, None) ], b) ->
+  | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement) ], b) ->
       let str_tk = Kindops.string_of_theorem_kind tk in
       let str_id = Id.to_string id in
       (xmlThm str_tk str_id loc [pp_expr statement])
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 25d3c705f4..d62c639c2e 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -209,7 +209,7 @@ type one_inductive_expr =
   plident * local_binder_expr list * constr_expr option * constructor_expr list
 
 type proof_expr =
-  plident option * (local_binder_expr list * constr_expr * (lident option * recursion_order_expr) option)
+  plident option * (local_binder_expr list * constr_expr)
 
 type syntax_modifier =
   | SetItemLevel of string list * Extend.production_level
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 71b93439bc..6ede0490e4 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -146,8 +146,8 @@ GEXTEND Gram
     [ [ thm = thm_token; id = pidentref; bl = binders; ":"; c = lconstr;
         l = LIST0
           [ "with"; id = pidentref; bl = binders; ":"; c = lconstr ->
-          (Some id,(bl,c,None)) ] ->
-          VernacStartTheoremProof (thm, (Some id,(bl,c,None))::l, false)
+          (Some id,(bl,c)) ] ->
+          VernacStartTheoremProof (thm, (Some id,(bl,c))::l, false)
       | stre = assumption_token; nl = inline; bl = assum_list ->
 	  VernacAssumption (stre, nl, bl)
       | (kwd,stre) = assumptions_token; nl = inline; bl = assum_list ->
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index cfc2e48d11..d3b4007fbe 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -386,13 +386,12 @@ open Decl_kinds
     ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr def) def
     ++ prlist (pr_decl_notation pr_constr) ntn
 
-  let pr_statement head (idpl,(bl,c,guard)) =
+  let pr_statement head (idpl,(bl,c)) =
     assert (not (Option.is_empty idpl));
     let id, pl = Option.get idpl in
     hov 2
       (head ++ spc() ++ pr_lident id ++ pr_univs pl ++ spc() ++
          (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
-         pr_opt (pr_guard_annot pr_lconstr_expr bl) guard ++
          str":" ++ pr_spc_lconstr c)
 
   let pr_priority = function
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 409676276a..e7d1919ce0 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -88,25 +88,9 @@ let adjust_guardness_conditions const = function
 
 let find_mutually_recursive_statements thms =
     let n = List.length thms in
-    let inds = List.map (fun (id,(t,impls,annot)) ->
+    let inds = List.map (fun (id,(t,impls)) ->
       let (hyps,ccl) = decompose_prod_assum t in
       let x = (id,(t,impls)) in
-      match annot with
-      (* Explicit fixpoint decreasing argument is given *)
-      | Some (Some (_,id),CStructRec) ->
-          let i,b,typ = lookup_rel_id id hyps in
-          (match kind_of_term t with
-          | Ind ((kn,_ as ind), u) when
-              let mind = Global.lookup_mind kn in
-              mind.mind_finite == Decl_kinds.Finite && Option.is_empty b ->
-              [ind,x,i],[]
-          | _ ->
-              error "Decreasing argument is not an inductive assumption.")
-      (* Unsupported cases *)
-      | Some (_,(CWfRec _|CMeasureRec _)) ->
-          error "Only structural decreasing is supported for mutual statements."
-      (* Cofixpoint or fixpoint w/o explicit decreasing argument *)
-      | None | Some (None, CStructRec) ->
       let whnf_hyp_hds = map_rel_context_in_env
         (fun env c -> fst (whd_all_stack env Evd.empty c))
         (Global.env()) hyps in
@@ -178,7 +162,7 @@ let find_mutually_recursive_statements thms =
     (finite,guard,None), ordered_inds
 
 let look_for_possibly_mutual_statements = function
-  | [id,(t,impls,None)] ->
+  | [id,(t,impls)] ->
       (* One non recursively proved theorem *)
       None,[id,(t,impls)],None
   | _::_ as thms ->
@@ -458,7 +442,7 @@ let start_proof_com ?inference_hook kind thms hook =
 		    | None -> Evd.from_env env0
 		    | Some l -> Evd.from_ctx (Evd.make_evar_universe_context env0 l))
   in
-  let thms = List.map (fun (sopt,(bl,t,guard)) ->
+  let thms = List.map (fun (sopt,(bl,t)) ->
     let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
     let t', imps' = interp_type_evars_impls ~impls env evdref t in
     let flags = all_and_fail_flags in
@@ -467,8 +451,7 @@ let start_proof_com ?inference_hook kind thms hook =
     let ids = List.map RelDecl.get_name ctx in
       (compute_proof_name (pi1 kind) sopt,
       (nf_evar !evdref (it_mkProd_or_LetIn t' ctx),
-       (ids, imps @ lift_implicits (List.length ids) imps'),
-       guard)))
+       (ids, imps @ lift_implicits (List.length ids) imps'))))
     thms in
   let recguard,thms,snl = look_for_possibly_mutual_statements thms in
   let evd, nf = Evarutil.nf_evars_and_universes !evdref in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ca03ba3f3a..07066d983d 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -489,7 +489,7 @@ let vernac_definition locality p (local,k) ((loc,id as lid),pl) def =
   (match def with
     | ProveBody (bl,t) ->   (* local binders, typ *)
 	  start_proof_and_print (local,p,DefinitionBody k)
-	    [Some (lid,pl), (bl,t,None)] hook
+	    [Some (lid,pl), (bl,t)] hook
     | DefineBody (bl,red_option,c,typ_opt) ->
  	let red_option = match red_option with
           | None -> None
@@ -2077,7 +2077,7 @@ let interp ?proof ~loc locality poly c =
   | VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n")
 
   (* Proof management *)
-  | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t,None)] false
+  | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t)] false
   | VernacFocus n -> vernac_focus n
   | VernacUnfocus -> vernac_unfocus ()
   | VernacUnfocused -> vernac_unfocused ()
-- 
cgit v1.2.3


From 70930579d8454a4ff50ee0ea1e97a55863bf01f6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Apr 2017 15:53:14 +0200
Subject: More explicit message when a {struct x} argument refers to a local
 definition.

---
 interp/topconstr.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 89e04b69d2..513fa8f161 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -176,7 +176,12 @@ let split_at_annot bl na =
               in
               (List.rev ans, CLocalAssum (r, k, t) :: rest)
             end
-	| CLocalDef _ as x :: rest -> aux (x :: acc) rest
+	| CLocalDef ((_,na),_,_) as x :: rest ->
+           if Name.equal (Name id) na then
+             user_err ~loc
+               (Nameops.pr_id id ++ str" must be a proper parameter and not a local definition.")
+           else
+             aux (x :: acc) rest
         | CLocalPattern (loc,_,_) :: rest ->
             Loc.raise ~loc (Stream.Error "pattern with quote not allowed after fix")
 	| [] ->
-- 
cgit v1.2.3


From 8d69323dff6e1afd17a13dfa8a980e76acb44cdc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Apr 2017 15:53:35 +0200
Subject: Documenting how the recursive indices of a fixpoint are computed.

Also documenting how the implicit arguments by position are computed.
---
 intf/constrexpr.mli | 2 +-
 kernel/constr.ml    | 9 +++++++++
 2 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index 49bafadc8e..a4a6eb9092 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -19,7 +19,7 @@ open Decl_kinds
 type notation = string
 
 type explicitation =
-  | ExplByPos of int * Id.t option
+  | ExplByPos of int * Id.t option (* a reference to the n-th product starting from left *)
   | ExplByName of Id.t
 
 type binder_kind =
diff --git a/kernel/constr.ml b/kernel/constr.ml
index ce20751abc..d0c580d138 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -107,7 +107,16 @@ type constr = t
 type existential = existential_key * constr array
 type rec_declaration = Name.t array * constr array * constr array
 type fixpoint = (int array * int) * rec_declaration
+  (* The array of [int]'s tells for each component of the array of
+     mutual fixpoints the number of lambdas to skip before finding the
+     recursive argument (e.g., value is 2 in "fix f (x:A) (y:=t) (z:B)
+     (v:=u) (w:I) {struct w}"), telling to skip x and z and that w is
+     the recursive argument);
+     The second component [int] tells which component of the block is
+     returned *)
 type cofixpoint = int * rec_declaration
+  (* The component [int] tells which component of the block of
+     cofixpoint is returned *)
 
 type types = constr
 
-- 
cgit v1.2.3


From 8a35d93061c67dcdbb12337b78fcb35d72957f51 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Apr 2017 19:13:33 +0200
Subject: Minor cosmetic commit.

---
 vernac/command.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/vernac/command.ml b/vernac/command.ml
index 6eb7037f84..f31fce8859 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -1155,7 +1155,7 @@ let interp_fixpoint l ntns =
 
 let interp_cofixpoint l ntns =
   let (env,_,pl,evd),fix,info = interp_recursive false l ntns in
-  check_recursive false  env evd fix;
+  check_recursive false env evd fix;
   (fix,pl,Evd.evar_universe_context evd,info)
     
 let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
-- 
cgit v1.2.3


From 21d308fc083ee395e7b1ff78e75ec3a1305cb2f4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Apr 2017 19:12:44 +0200
Subject: Fixing several wrong computations of implicit arguments by position
 in the presence of let-ins.

---
 test-suite/success/ImplicitArguments.v | 6 ++++++
 vernac/command.ml                      | 6 +++---
 vernac/lemmas.ml                       | 2 +-
 3 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v
index f702aa62f1..f07773f8bd 100644
--- a/test-suite/success/ImplicitArguments.v
+++ b/test-suite/success/ImplicitArguments.v
@@ -21,3 +21,9 @@ Fixpoint app {A : Type} {n m : nat} (v : vector A n) (w : vector A m) : vector A
 (* Test sharing information between different hypotheses *)
 
 Parameters (a:_) (b:a=0).
+
+(* These examples were failing due to a lifting wrongly taking let-in into account *)
+
+Definition foo6 (x:=1) : forall {n:nat}, n=n := fun n => eq_refl.
+
+Fixpoint foo7 (x:=1) (n:nat) {p:nat} {struct n} : nat.
diff --git a/vernac/command.ml b/vernac/command.ml
index f31fce8859..c24dbdf7c0 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -95,7 +95,7 @@ let interp_definition pl bl p red_option c ctypopt =
   let ctx = Evd.make_evar_universe_context env pl in
   let evdref = ref (Evd.from_ctx ctx) in
   let impls, ((env_bl, ctx), imps1) = interp_context_evars env evdref bl in
-  let nb_args = List.length ctx in
+  let nb_args = Context.Rel.nhyps ctx in
   let imps,pl,ce =
     match ctypopt with
       None ->
@@ -838,7 +838,7 @@ type structured_fixpoint_expr = {
 let interp_fix_context env evdref isfix fix =
   let before, after = if isfix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in
   let impl_env, ((env', ctx), imps) = interp_context_evars env evdref before in
-  let impl_env', ((env'', ctx'), imps') = interp_context_evars ~impl_env ~shift:(List.length before) env' evdref after in
+  let impl_env', ((env'', ctx'), imps') = interp_context_evars ~impl_env ~shift:(Context.Rel.nhyps ctx) env' evdref after in
   let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in
     ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot)
 
@@ -1100,7 +1100,7 @@ let interp_recursive isfix fixl notations =
   let fixtypes = List.map2 build_fix_type fixctxs fixccls in
   let fixtypes = List.map (nf_evar !evdref) fixtypes in
   let fiximps = List.map3
-    (fun ctximps cclimps (_,ctx) -> ctximps@(Impargs.lift_implicits (List.length ctx) cclimps))
+    (fun ctximps cclimps (_,ctx) -> ctximps@(Impargs.lift_implicits (Context.Rel.nhyps ctx) cclimps))
     fixctximps fixcclimps fixctxs in
   let rec_sign =
     List.fold_left2
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index e7d1919ce0..430d48bc76 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -451,7 +451,7 @@ let start_proof_com ?inference_hook kind thms hook =
     let ids = List.map RelDecl.get_name ctx in
       (compute_proof_name (pi1 kind) sopt,
       (nf_evar !evdref (it_mkProd_or_LetIn t' ctx),
-       (ids, imps @ lift_implicits (List.length ids) imps'))))
+       (ids, imps @ lift_implicits (Context.Rel.nhyps ctx) imps'))))
     thms in
   let recguard,thms,snl = look_for_possibly_mutual_statements thms in
   let evd, nf = Evarutil.nf_evars_and_universes !evdref in
-- 
cgit v1.2.3


From 2ddc9d12bd4616f10245c40bc0c87ae548911809 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Apr 2017 19:13:58 +0200
Subject: 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.
---
 doc/refman/RefMan-tac.tex |  6 +++---
 tactics/tactics.ml        |  3 +++
 vernac/command.ml         | 16 +++++++++-------
 vernac/command.mli        |  8 ++++----
 vernac/lemmas.ml          |  4 ++--
 vernac/lemmas.mli         |  4 ++--
 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 :
-- 
cgit v1.2.3