else if conclude.Con.conclude_method = "FalseInd" then
(* false ind is in charge to add the conclusion *)
falseind conclude
else if conclude.Con.conclude_method = "FalseInd" then
(* false ind is in charge to add the conclusion *)
falseind conclude
- (make_concl "to prove" proof_conclusion) in
- B.V ([], induction_on::to_prove:: B.Text([],".")::(make_cases args_for_cases))
+ B.H ([], [make_concl "to prove" proof_conclusion ; B.Text([],".")]) in
+ B.V ([], induction_on::to_prove::(make_cases args_for_cases))
- B.V ([], pattern::induction_hypothesis@[asubconcl;B.Text([],".");presacontext])
+ B.V ([], pattern::induction_hypothesis@[B.H ([],[asubconcl;B.Text([],".")]);presacontext])
[Some "helm","xref","id"]
([ B.b_h [] (B.b_kw ("theorem " ^ name) ::
params2pres params @ [B.b_kw ":"]);
[Some "helm","xref","id"]
([ B.b_h [] (B.b_kw ("theorem " ^ name) ::
params2pres params @ [B.b_kw ":"]);
metasenv2pres term2pres metasenv @
[proof ; B.b_kw "qed."])
| `Def (_, ty, `Definition body) ->
metasenv2pres term2pres metasenv @
[proof ; B.b_kw "qed."])
| `Def (_, ty, `Definition body) ->