aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
Commit message (Expand)AuthorAge
* 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
* | Clarifying and documenting the UState API.Gravatar Pierre-Marie Pédrot2015-10-17
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-15
|\|
| * When typechecking a lemma statement, try to resolve typeclasses beforeGravatar Matthieu Sozeau2015-10-14
* | 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
| * TQueue: Allow some tasks to be saved when clearing a TQueueGravatar Alec Faithfull2015-10-09
| * TQueue: Expose the length of TQueuesGravatar 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
|\|
| * Axioms now support the universe binding syntax.Gravatar Pierre-Marie Pédrot2015-10-08
| * Proof using: let-in policy, optional auto-clear, forward closure*Gravatar Enrico Tassi2015-10-08
| * Spawn: use each socket exclusively for writing or readingGravatar 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
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|\|
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|\ \
| | * Univs: fix semantics of Type in proof mode in universe-polymorphic modeGravatar Matthieu Sozeau2015-10-02
| | * Univs: fix handling of side effects/delayed proofsGravatar Matthieu Sozeau2015-10-02
| | * Univs: fix many evar_map initializations and leaks.Gravatar Matthieu Sozeau2015-10-02
| |/
| * Remove some uses of Loadpath.get_paths.Gravatar Guillaume Melquiond2015-09-29
* | Hardening the API of evarmaps.Gravatar Pierre-Marie Pédrot2015-09-26
* | Rich printing of messages.Gravatar Pierre-Marie Pédrot2015-09-20
* | Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-09-17
|\|
| * STM: Reset takes Ltac <ident> into account (Close #4316)Gravatar Enrico Tassi2015-09-15
| * Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
* | More potentialities in proof_terminators.Gravatar Pierre-Marie Pédrot2015-09-08
* | Opacifying the proof_terminator type.Gravatar Pierre-Marie Pédrot2015-09-08
|/
* STM: save a full state for queries.Gravatar Enrico Tassi2015-09-01
* Removing code duplication in Lemmas.Gravatar Pierre-Marie Pédrot2015-08-19
* Documentation by giving a name to a large type.Gravatar Pierre-Marie Pédrot2015-08-19
* 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
* Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Gravatar Lionel Rieg2015-06-26
* Splitting the library representation on disk in two.Gravatar Pierre-Marie Pédrot2015-06-24
* 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
* Admitted does not drop poly-univ constraints (Fix #4244)Gravatar Enrico Tassi2015-06-03
* STM: preserve branch name on edit (Close: #4245, #4246)Gravatar Enrico Tassi2015-05-28
* Fix bug #4159Gravatar Matthieu Sozeau2015-05-27
* 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