aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
Commit message (Expand)AuthorAge
* STM: primitives to snapshot a .vi while in interactive modeGravatar Enrico Tassi2014-10-13
* TQueue: new primitive to take a snapshot of the queueGravatar Enrico Tassi2014-10-13
* STM: simplify how the term part of a side effect is retrievedGravatar Enrico Tassi2014-10-13
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* STM: report the (structured) goals as XMLGravatar Carst Tankink2014-10-01
* Add additional location information to AST XMLs.Gravatar Carst Tankink2014-10-01
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* XML pretty printing for AST (work by François Poulain, project DoCoq)Gravatar Enrico Tassi2014-09-29
* Notation: option to attach extra pretty printing rules to notationsGravatar Enrico Tassi2014-09-29
* Undo prints only if coqtop || emacsGravatar Enrico Tassi2014-09-16
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* VernacExtend does not dispatch on type anymore.Gravatar Pierre-Marie Pédrot2014-09-10
* Marshalling errors should be bold and red (should never happen actually)Gravatar Enrico Tassi2014-09-09
* A marshalling failure does not make a worker `OldGravatar Enrico Tassi2014-09-09
* Back: print subgoals as in 8.4 (Close: 3585)Gravatar Enrico Tassi2014-09-09
* BackTo not part of the doc when used by emacsGravatar Enrico Tassi2014-09-09
* Undo: if the ui is coqtop (command line) then Undo is not part of the doc.Gravatar Enrico Tassi2014-09-09
* Dropped proofs (Abort) are evaluated synchronously (Closes: 3550, 3407)Gravatar Enrico Tassi2014-09-09
* Remove [Infer] option of records.Gravatar Arnaud Spiwack2014-09-04
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
* stm: use xlabel insted of label in dot (debug) outputGravatar Enrico Tassi2014-09-02
* coqworkmgrGravatar Enrico Tassi2014-09-02
* Do not pass "-batch" or "-load-vernac-source" to slaves, avoiding errors inGravatar Matthieu Sozeau2014-08-26
* STM: new "par:" goal selector, like "all:" but in parallelGravatar Enrico Tassi2014-08-05
* STM: code restructured to reuse task queue for tacticsGravatar Enrico Tassi2014-08-05
* STM: Classify Let as non asynchronous (Closes: #3486)Gravatar Enrico Tassi2014-08-05
* STM: when looking up in the cache catch Expired excGravatar Carst Tankink2014-08-04
* STM: generate Feedback message for parsing errorsGravatar Enrico Tassi2014-08-04
* STM: use a real priority queueGravatar Enrico Tassi2014-08-04
* STM: encapsulate Pp.message in Feedback.feedbackGravatar Carst Tankink2014-08-04
* STM: VtQuery holds the id of the state it refers toGravatar Carst Tankink2014-08-04
* STM: print goals with no duplicatesGravatar Enrico Tassi2014-07-29
* Fixing universe substitution in mutual fixpoints.Gravatar Pierre-Marie Pédrot2014-07-16
* STM: check-vi-task fixedGravatar Enrico Tassi2014-07-16
* STM: Goal printing got wrong in a merge, fixedGravatar Enrico Tassi2014-07-16
* STM: let toploop plugins specify the flags for STM workersGravatar Enrico Tassi2014-07-11
* STM: flag to turn off branch reopeningGravatar Enrico Tassi2014-07-11
* STM: add optionally takes the id of the new tipGravatar Enrico Tassi2014-07-11
* STM: export the observe function (useful for pide)Gravatar Enrico Tassi2014-07-11
* Feedback: LoadedFile + GoalsGravatar Enrico Tassi2014-07-11
* Better handling of the universe context in case of Admitted proof obligations.Gravatar Matthieu Sozeau2014-07-10
* option to always delegate futures to workersGravatar Enrico Tassi2014-07-10
* more APIs in TQueue and CThreadGravatar Enrico Tassi2014-07-10
* Add toplevel commands to declare global universes and constraints.Gravatar Matthieu Sozeau2014-07-01
* Patch from Enrico Tassi to get Drop compatible with stm.Gravatar Enrico Tassi2014-07-01
* Typo in stm error message.Gravatar Hugo Herbelin2014-06-28
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-06-25
* cut toploop(s) out of coqtop: now they are loaded dynamicallyGravatar Enrico Tassi2014-06-25
* Fix handling of side effects in Defined objects (Closes: HoTT#111 + 3344)Gravatar Enrico Tassi2014-06-23
* Proofs now take and return an evar_universe_context, simplifying interfacesGravatar Matthieu Sozeau2014-06-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 23:12:32 +0000