hammer and sauto output in response window don't give non-CoqHammer code meant to replace hammer and sauto statements.

[pr28416]

Hi,

According to the documentation, "The intended use of the hammer tactic is to replace it upon success with the reconstruction tactic shown in the response window. This reconstruction tactic has no time limits and makes no calls to external ATPs." But when I successfully run sauto, there is no response window output, and when I run hammer, the output often includes a "replace with sauto/hauto" or something similar, which isn't too descriptive of what non-"auto" code might replace the sauto or hammer statement.

Example:

Require Import Arith.
Lemma lem_odd : forall n : nat, Nat.Odd n \/ Nat.Odd (n + 1).
Proof.
  hammer.
Qed.

Output:

Replace the hammer tactic with:
    hauto use: Nat.Odd_add_r, Nat.add_1_r, Nat.odd_spec, Nat.mul_0_r, Nat.Even_or_Odd unfold: Nat.Odd, Init.Nat.odd.

In this case, shouldn't it instead be the case that one can view non-"auto" code that should replace the "hammer" command, not something that includes "hauto"?

[lukaszcz]

What's so hard to understand about this? You should replace the "hammer" tactic with what is suggested, which is usually some version of sauto/hauto - these are the reconstruction tactics which don't have time limits and don't depend on external ATPs.