| Remove deprecated comments. |
|
More...
|
over 6 years ago
|
| proposition de nouvelle fonction exportée dans controller_itp |
|
More...
|
over 6 years ago
|
| Extraction: new label [ocaml:remove] |
|
More...
|
over 6 years ago
|
| Useless cases in scheduling |
|
More...
|
over 6 years ago
|
| proof scripts: text of goal must be modified when input source changes |
|
More...
|
over 6 years ago
|
| blocking is a new parameter of module type scheduler. |
|
More...
|
over 6 years ago
|
| menage: plus de UnEdited et JustEdited |
|
More...
|
over 6 years ago
|
| Using new forward_result to get new results from why3server. |
|
More...
|
over 6 years ago
|
| second time edition indeed works now |
|
More...
|
over 6 years ago
|
| editing and replaying proofs with interactive provers, works better |
|
More...
|
over 6 years ago
|
| fix several pbs with interactive provers replay and proof scripts edition |
|
More...
|
over 6 years ago
|
| update session with polypaver |
|
More...
|
over 6 years ago
|
| Improving support for detached theories and goals |
|
More...
|
over 6 years ago
|
| avoid silent failures in presence of detached theories |
|
More...
|
over 6 years ago
|
| Adapt to Coq 8.7. |
|
More...
|
over 6 years ago
|
| Extraction: error location for failed extraction of [val] declarations |
|
More...
|
over 6 years ago
|
| When focus is not yet defined, notify still sends notification that are not node-specific. |
|
More...
|
over 6 years ago
|
| Allow focusing on several nodes at once. |
|
More...
|
over 6 years ago
|
| Extraction test: commented [val] declaration that was never used. |
|
More...
|
over 6 years ago
|
| Extraction: test if a [val] declaration is assigned in the driver |
|
More...
|
over 6 years ago
|
| Schorr Waite: two functions marked ghost as they are only used in ghost code |
|
More...
|
over 6 years ago
|
| Port examples/f_puzzle. |
|
More...
|
over 6 years ago
|
| Extraction |
|
More...
|
over 6 years ago
|
| ebauche de bisect |
|
More...
|
over 6 years ago
|
| Adapted to Isabelle2017 |
|
More...
|
over 6 years ago
|
| why3replay displays progress, unless -q is set |
|
More...
|
over 6 years ago
|
| update proofs that where made with bisect before that now work easily |
|
More...
|
over 6 years ago
|
| adapted limits should not be stored in session |
|
More...
|
over 6 years ago
|
| Removed task_driver. Currently, Pretty is used to print tasks. |
|
More...
|
over 6 years ago
|
| Changing adatp_limits so that we keep the steps limit even in failing cases. |
|
More...
|
over 6 years ago
|
