Le 03/04/2019 à 10:22, Julia Lawall a écrit : > On Wed, 3 Apr 2019, Sylvain Dailler wrote: >> >> Perhaps, we should hide this kind of transformations from the IDE ? >>> Is >>> there a way to click once and get them all to be proved at once? >> >> After a transformation is completed, if you want to use a command on all its >> subnodes, you can first click the transformation node and then use the >> command >> as normal. By default, this will execute your command on all the subgoals. >> Alternatively, you can right click on the transformation node and launch your >> command from there. > > As mentioned in my other response, this doesn't work properly when there > is a split. Perhaps the source of the problem is that typing > smoke-detector into the command line box doesn't do the same thing as when > the smoke detector is run on the real command line with replay. >
So perhaps you both agree that we should hide the smoke detector transformation but we should not hide the smoke detector functionnality in the IDE. The difficulty is too change the way the consolidation of the tree is done by adding an "inconsistent if reachable" value. -- François _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
