I have two laptops, one at home, one at work. I tried saving the state
(foo subdirectory, for a foo.mlw file) with git on my home machine, and
pulling onto my work machine. Part of my state is a coq proof. But when
I start up why3 at work and select coq, it asks me to make a new proof,
rather th
Le 19/02/2018 à 11:43, Julia Lawall a écrit :
I have two laptops, one at home, one at work. I tried saving the state
(foo subdirectory, for a foo.mlw file) with git on my home machine, and
pulling onto my work machine. Part of my state is a coq proof. But when
I start up why3 at work and selec
On Mon, 19 Feb 2018, Guillaume Melquiond wrote:
> Le 19/02/2018 à 11:43, Julia Lawall a écrit :
> > I have two laptops, one at home, one at work. I tried saving the state
> > (foo subdirectory, for a foo.mlw file) with git on my home machine, and
> > pulling onto my work machine. Part of my st
Le 19/02/2018 à 13:59, Julia Lawall a écrit :
Sorry, I don't understand the sequence of operations. First I start up
why3 ide. Then I click on my goal and then on Coq. This gives me a Coq
line with (not yet edited). In the tools menu, I found "Mark as
obsolete". After clicking on that I get
On Mon, 19 Feb 2018, Guillaume Melquiond wrote:
> Le 19/02/2018 à 13:59, Julia Lawall a écrit :
>
> > Sorry, I don't understand the sequence of operations. First I start up
> > why3 ide. Then I click on my goal and then on Coq. This gives me a Coq
> > line with (not yet edited). In the tools
Le 19/02/2018 à 13:59, Julia Lawall a écrit :
> Sorry, I don't understand the sequence of operations. First I start up
> why3 ide. Then I click on my goal and then on Coq. This gives me a Coq
> line with (not yet edited). In the tools menu, I found "Mark as
> obsolete". After clicking on tha
Le 19/02/2018 à 14:20, Julia Lawall a écrit :
> It does not appear. It does work when I move from one clone of the git
> repository to another on the same machine. I'll see later what happens
> when I move to a different machine. I think that the versions of Coq are
> the same (have the same nu
On Mon, 19 Feb 2018, Claude Marché wrote:
>
>
> Le 19/02/2018 à 13:59, Julia Lawall a écrit :
> > Sorry, I don't understand the sequence of operations. First I start up
> > why3 ide. Then I click on my goal and then on Coq. This gives me a Coq
> > line with (not yet edited). In the tools men
