> > First question: how do I inform Why3 that this
> > particular goal was actually proved? It seems that "Tools | Replay
> > valid obsolete proofs" does this, but can I do this one goal at a
> > time?
>
> Just run Coq again on your goal.
I am not sure how to do this. When I right-click on the goa
Le 10/05/2019 à 12:57, Евгений Макаров a écrit :
Hello,
I don't fully understand how to invoke Coq from Why3. Suppose I am
working on examples/logic/hello_proof.why. I right-click goal G3 and
select "Coq 8.9.0". CoqIDE starts. I fill in a proof between Proof and
Qed, save the file and quit CoqID
Hello,
I don't fully understand how to invoke Coq from Why3. Suppose I am
working on examples/logic/hello_proof.why. I right-click goal G3 and
select "Coq 8.9.0". CoqIDE starts. I fill in a proof between Proof and
Qed, save the file and quit CoqIDE. The proof attempt by Coq in Why3
is marked obsol
