aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/stm.ml
Commit message (Expand)AuthorAge
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-05
|\
| * Follow-up fix on Enrico's 6e376c8097d75b6e, with Enrico.Gravatar Maxime Dénès2015-11-02
| * STM: fix undo into a branch containing side effectsGravatar Enrico Tassi2015-11-02
| * STM: never reopen a branch containing side effectsGravatar Enrico Tassi2015-11-02
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-30
|\|
| * Add a way to get the right fix_exn in external vernacular commandsGravatar Matthieu Sozeau2015-10-30
| * Handle side-effects of Vernacular commands inside proofs better, so thatGravatar Matthieu Sozeau2015-10-29
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-19
|\|
| * Miscellaneous typos, spacing, US spelling in comments or variable names.Gravatar Hugo Herbelin2015-10-18
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-10
|\|
| * STM: Work around an occasional crash in dot (debug output)Gravatar Alec Faithfull2015-10-09
| * STM: Added functions for saving and restoring the internal stateGravatar Alec Faithfull2015-10-09
| * STM: Pass exception information to unreachable_state_hook functionsGravatar Alec Faithfull2015-10-09
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-09
|\|
| * Proof using: let-in policy, optional auto-clear, forward closure*Gravatar Enrico Tassi2015-10-08
| * STM: for PIDE based UIs, edit_at requires no Reach.known_stateGravatar Enrico Tassi2015-10-08
| * STM: fix backtrace handlingGravatar Enrico Tassi2015-10-08
* | Hardening the API of evarmaps.Gravatar Pierre-Marie Pédrot2015-09-26
|/
* Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
* STM: save a full state for queries.Gravatar Enrico Tassi2015-09-01
* STM: make multiple, admitted, nested proofs work (fix #4314)Gravatar Enrico Tassi2015-07-30
* STM: emit a warning when a QED/Admitted proof contains a nested lemmaGravatar Enrico Tassi2015-07-30
* STM: fix backtrack in presence of nested, immediate, proofsGravatar Enrico Tassi2015-07-30
* STM: remove assertion not being true for nested, immediate, proofs (#4313)Gravatar Enrico Tassi2015-07-30
* Fixing what seems to be a typo.Gravatar Hugo Herbelin2015-07-29
* ShowScript: as 8.4 w.r.t. unnamed proofs and non tactic vernacs (fix #4308)Gravatar Enrico Tassi2015-07-28
* STM: fix a "exn with no safe id attached" error on a failing queryGravatar Enrico Tassi2015-07-14
* STM: states coming from workers have no proof terminators (Close #4246)Gravatar Enrico Tassi2015-06-09
* STM: silly mistake in jumping back to an old state (Close #4249)Gravatar Enrico Tassi2015-06-09
* STM: preserve branch name on edit (Close: #4245, #4246)Gravatar Enrico Tassi2015-05-28
* nice error for Restart outside a proof (Close: #4235)Gravatar Enrico Tassi2015-05-12
* Add a [Redirect] vernacular commandGravatar Clément Pit--Claudel2015-05-04
* STM: print trace on "anomaly, no safe id attached"Gravatar Enrico Tassi2015-04-21
* CoqIDE: simpler way of reopening/reclosing a proof (Close: 4168)Gravatar Enrico Tassi2015-04-02
* STM: refine the notion of "simply a tactic"Gravatar Enrico Tassi2015-03-27
* STM: change how proof mode switching commands are handled (decl_mode)Gravatar Enrico Tassi2015-03-26
* STM: avoid processing asynchronously empty proofs (Close: #4134)Gravatar Enrico Tassi2015-03-25
* STM: if Set Universe Polymorphism then synchronous (#4119)Gravatar Enrico Tassi2015-03-22
* STM: do not delegate proofs containing PrintGravatar Enrico Tassi2015-03-22
* STM: after every command restore the expected proof modeGravatar Enrico Tassi2015-03-22
* Fixed #4138. In emacs mode Set/Unset does not print the goal anymore.Gravatar Pierre Courtieu2015-03-20
* STM: -debug: better explanation of why not async (#4125)Gravatar Enrico Tassi2015-03-15
* STM: -quick: async no Proof using but no Section (#4124)Gravatar Enrico Tassi2015-03-15
* STM: ease re-editing of Admitted proofsGravatar Enrico Tassi2015-03-11
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* STM: Considering Stack_overflow as a normal tactic error (Close #3576)Gravatar Enrico Tassi2015-02-27
* STM: proof state also includes meta countersGravatar Enrico Tassi2015-02-25
* Future: human readable name for delegated (Close #4065)Gravatar Enrico Tassi2015-02-21
* STM: when async_proofs_full is set process only tasks in the perspectiveGravatar Enrico Tassi2015-02-16
* Undo: back to 8.4 semantics (Close #3514)Gravatar Enrico Tassi2015-02-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 12:37:40 +0000