- 15 Nov, 2016 1 commit
-
-
Clément Fumex authored
-
- 14 Nov, 2016 2 commits
-
-
Sylvain Dailler authored
-
Sylvain Dailler authored
Also put the selection on first subgoal when applying transformation.
-
- 10 Nov, 2016 3 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
Sylvain Dailler authored
Complete creation of the tree session in ide(todo: decide what to print). Added a table proofnodeID -> gtk_tree_iter to provide to callbacks. Added callbacks that change the IDE output.
-
- 09 Nov, 2016 3 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
Clément Fumex authored
-
- 08 Nov, 2016 2 commits
-
-
Sylvain Dailler authored
Also, added a debug flag to be raised when matching of apply fail. To do that, I changed exception NoMatch so that it returns the terms that cant be matched. This needs some testing.
-
Sylvain Dailler authored
Added a last set which is build at the same time of the name_tables which is a map from id to list of decls where id is used. This has to be tested if this is actually efficient (time and memory). If not, we can still disallow it with a boolean.
-
- 07 Nov, 2016 4 commits
-
-
Sylvain Dailler authored
Ident closer to the goal have lower disambiguation numbers. We do that by first puting all declarations in a list and then iter on it. Also removing useless comments in test_argument and args_wrapper.
-
Sylvain Dailler authored
-
Sylvain Dailler authored
present.
-
Sylvain Dailler authored
-
- 04 Nov, 2016 3 commits
-
-
Sylvain Dailler authored
-
Sylvain Dailler authored
-
Sylvain Dailler authored
* call_provers.ml (prover_update): Adding unimplemented errors that reflects the cases of proof_attempt_status. Otherwise, proof_attempt_status is a list of cases that are never reached. * controller_itp.ml (proof_attempt_status): Added Uninstalled case in proof_attempt_status. Launched in replay when asked to replay something not installed. (print_trans_status): Adding a ! when proof is valid for debugging reasons. (report): Added a report type for replay reporting of differences. (print_report): printing function for report. (replay_print): callback used with replay to print the report at the end. (replay): Function that replays all proof attempts of the session. * session_itp.ml (session_iter_proof_attempt): Added the proofNodeID the fold function for convenience. * why3shell.ml (test_replay): Added to test replay.
-
- 03 Nov, 2016 6 commits
-
-
Sylvain Dailler authored
-
Sylvain Dailler authored
Possibility to add env to transformation via args_wrapper (ugly).
-
Sylvain Dailler authored
-
Sylvain Dailler authored
-
Sylvain Dailler authored
-
Sylvain Dailler authored
-
- 02 Nov, 2016 2 commits
-
-
MARCHE Claude authored
-
Sylvain Dailler authored
Rewrite and replace.
-
- 28 Oct, 2016 1 commit
-
-
Clément Fumex authored
-
- 27 Oct, 2016 2 commits
-
-
MARCHE Claude authored
-
Clément Fumex authored
-
- 26 Oct, 2016 3 commits
-
-
Sylvain Dailler authored
Seemed useful because the declaration might not be displayed.
-
Sylvain Dailler authored
On some examples, goal was cut when first end was encountered.
-
Clément Fumex authored
- add session directory and restore old session file mechanism
-
- 24 Oct, 2016 3 commits
-
-
Sylvain Dailler authored
-
Sylvain Dailler authored
-
Sylvain Dailler authored
-
- 21 Oct, 2016 4 commits
-
-
MARCHE Claude authored
-
Sylvain Dailler authored
-
Sylvain Dailler authored
I think it is currently passed into the command.
-
MARCHE Claude authored
-
- 20 Oct, 2016 1 commit
-
-
Sylvain Dailler authored
-