Hey all,

I've been using the `Set Suggest Proof Using`

flag in coq to get Proof using annotations for proofs, which I then insert into proof files to allow automation to skip proofs reliably. But I noticed this doesn't seem to work for the obligations resulting from a Program statement. So, if you set that flag, and then run a program statement with holes, you get a bunch of obligations that you navigate with the `Next Obligation`

vernac. Depending on the holes, some of these can be filled with opaque objects, so you can use Qed to close them, or you can use Admitted to skip them. But like a normal proof, if you close it with Admitted without a `Proof using`

annotation, it'll assume it depends on all available section variables. And, like a normal proof, you can insert a `Proof using`

annotation to restrict this to a subset of the section variables, and then run Admitted, and it'll have the right type. *unlike* a normal proof though, the Set Suggest Proof Using flag won't suggest annotations for obligations opened with Next Obligation.

Is this a coq bug? Or intended behavior for some weird reason?

Proof using doesn't work for obligations, for instance

```
Axiom foo : nat -> True.
Section S.
Variable x : nat.
Program Definition bla : True := _.
Next Obligation.
Proof using .
apply foo,x.
Qed. (* accepted *)
```

I guess this is a bug

The bug is larger... `Proof using`

exists to help async processing, but that is not supporred for obligations. And in many cases, you'd want the same `using`

annotation for all obligations in a `Definition`

Last updated: Jun 23 2024 at 05:02 UTC