Recently I was told that there was a regression in the code for matching proofs to VCs on reloading a file. I did a pull and things seemed to work much better. But now I have the impression that things are not working so well again. For example, I have a goal that is just true, and it is associated to a proof that starts with inline. Has something changed again with respect to this issue, or is it just bad luck due to some other changes made on my side?
thanks, julia _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
