aboutsummaryrefslogtreecommitdiff
path: root/stm
AgeCommit message (Expand)Author
2014-10-01Add additional location information to AST XMLs.Carst Tankink
2014-09-30Add syntax for naming new goals in refine: writing ?[id] instead of _Hugo Herbelin
2014-09-29XML pretty printing for AST (work by François Poulain, project DoCoq)Enrico Tassi
2014-09-29Notation: option to attach extra pretty printing rules to notationsEnrico Tassi
2014-09-16Undo prints only if coqtop || emacsEnrico Tassi
2014-09-12Uniformisation of the order of arguments env and sigma.Hugo Herbelin
2014-09-10VernacExtend does not dispatch on type anymore.Pierre-Marie Pédrot
2014-09-09Marshalling errors should be bold and red (should never happen actually)Enrico Tassi
2014-09-09A marshalling failure does not make a worker `OldEnrico Tassi
2014-09-09Back: print subgoals as in 8.4 (Close: 3585)Enrico Tassi
2014-09-09BackTo not part of the doc when used by emacsEnrico Tassi
2014-09-09Undo: if the ui is coqtop (command line) then Undo is not part of the doc.Enrico Tassi
2014-09-09Dropped proofs (Abort) are evaluated synchronously (Closes: 3550, 3407)Enrico Tassi
2014-09-04Remove [Infer] option of records.Arnaud Spiwack
2014-09-04Print [Variant] types with the keyword [Variant].Arnaud Spiwack
2014-09-02stm: use xlabel insted of label in dot (debug) outputEnrico Tassi
2014-09-02coqworkmgrEnrico Tassi
2014-08-26Do not pass "-batch" or "-load-vernac-source" to slaves, avoiding errors inMatthieu Sozeau
2014-08-05STM: new "par:" goal selector, like "all:" but in parallelEnrico Tassi
2014-08-05STM: code restructured to reuse task queue for tacticsEnrico Tassi
2014-08-05STM: Classify Let as non asynchronous (Closes: #3486)Enrico Tassi
2014-08-04STM: when looking up in the cache catch Expired excCarst Tankink
2014-08-04STM: generate Feedback message for parsing errorsEnrico Tassi
2014-08-04STM: use a real priority queueEnrico Tassi
2014-08-04STM: encapsulate Pp.message in Feedback.feedbackCarst Tankink
2014-08-04STM: VtQuery holds the id of the state it refers toCarst Tankink
2014-07-29STM: print goals with no duplicatesEnrico Tassi
2014-07-16Fixing universe substitution in mutual fixpoints.Pierre-Marie Pédrot
2014-07-16STM: check-vi-task fixedEnrico Tassi
2014-07-16STM: Goal printing got wrong in a merge, fixedEnrico Tassi
2014-07-11STM: let toploop plugins specify the flags for STM workersEnrico Tassi
2014-07-11STM: flag to turn off branch reopeningEnrico Tassi
2014-07-11STM: add optionally takes the id of the new tipEnrico Tassi
2014-07-11STM: export the observe function (useful for pide)Enrico Tassi
2014-07-11Feedback: LoadedFile + GoalsEnrico Tassi
2014-07-10Better handling of the universe context in case of Admitted proof obligations.Matthieu Sozeau
2014-07-10option to always delegate futures to workersEnrico Tassi
2014-07-10more APIs in TQueue and CThreadEnrico Tassi
2014-07-01Add toplevel commands to declare global universes and constraints.Matthieu Sozeau
2014-07-01Patch from Enrico Tassi to get Drop compatible with stm.Enrico Tassi
2014-06-28Typo in stm error message.Hugo Herbelin
2014-06-25all coqide specific files moved into ide/Enrico Tassi
2014-06-25cut toploop(s) out of coqtop: now they are loaded dynamicallyEnrico Tassi
2014-06-23Fix handling of side effects in Defined objects (Closes: HoTT#111 + 3344)Enrico Tassi
2014-06-18Proofs now take and return an evar_universe_context, simplifying interfacesMatthieu Sozeau
2014-06-17Removing dead code.Pierre-Marie Pédrot
2014-06-08Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofPierre-Marie Pédrot
2014-06-08Enforce a correct exception handling in declaration_hooksEnrico Tassi
2014-06-08STM: handle "Time Abort" correctly (Closes: 3332)Enrico Tassi
2014-06-06Remove the syntax [Vernac1. Vernac2. … Vernacn. ].Arnaud Spiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 03:08:36 +0000