Commit 68a3301c authored by MARCHE Claude's avatar MARCHE Claude

Fix a few typos and details + ROADMAP

parent ee588657
......@@ -141,8 +141,8 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
* (JCF, ANDREI) add all examples from the VSTTE 2012 competition
* (CLAUDE) Ajouter page provers sur le site web why3
** DONE, merci de relire...
* DONE (CLAUDE) Ajouter page provers sur le site web why3
** merci de relire...
* Documentation
......@@ -159,20 +159,20 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
ident-executable
DONE remplacer le ":" par " " (Arg.Tuple)
- (CLAUDE) Documenter les popups qui peuvent apparaitre dans why3ide
- DONE (CLAUDE) Documenter les popups qui peuvent apparaitre dans why3ide
quand les prouveurs ont changé. Et les mettre au point:
. Lors d'un replay, le dialogue "replace proof" apparait un nombre
. DONE Lors d'un replay, le dialogue "replace proof" apparait un nombre
important de fois, il faut absolument pouvoir interrompre, ou
donner une reponse qui soit appliquée pour le reste. (le 3e
bouton "never replace..." ne semble pas jourer ce role...)
. le dialogue "replace proof" est de toute facon trop large, et les
. DONE le dialogue "replace proof" est de toute facon trop large, et les
choix possibles sont confus.
- (CLAUDE) meme ordre d'idee: ne pas ecraser "default editor" et
- DONE (CLAUDE) meme ordre d'idee: ne pas ecraser "default editor" et
"timelimit"
DONE, en fait c'était déjà le cas
en fait c'était déjà le cas
- (WHO?) complete api.tex: explain how to build theories, apply
transformations, write new functions on terms (A)
......
......@@ -753,7 +753,7 @@ let uninstalled_prover c eS unknown =
let others,names,versions = Session_tools.unknown_to_known_provers
(Whyconf.get_provers eS.Session.whyconf) unknown in
let dialog = GWindow.dialog
~icon:(!why_icon)
~icon:(!why_icon) ~modal:true
~title:"Why3: Uninstalled prover" ()
in
let vbox = dialog#vbox in
......@@ -763,8 +763,8 @@ let uninstalled_prover c eS unknown =
Pp.sprintf "The prover %a is not installed"
Whyconf.print_prover unknown
in
let _label1 = GMisc.label ~ypad:10 ~text ~xalign:0.5 ~packing:hb#add () in
let label = "Please select a policy for associated proof attemtps" in
let _label1 = GMisc.label ~ypad:20 ~text ~xalign:0.5 ~packing:hb#add () in
let label = "Please select a policy for associated proof attempts" in
let policy_frame = GBin.frame ~label ~packing:vbox#add () in
let choice = ref 0 in
let prover_choosed = ref None in
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment