aboutsummaryrefslogtreecommitdiff
path: root/stm
AgeCommit message (Expand)Author
2017-11-21[printing] Deprecate all printing functions accessing the global proof.Emilio Jesus Gallego Arias
2017-11-20Merge PR #6183: [plugins] Prepare plugin API for functional handling of state.Maxime Dénès
2017-11-20Merge PR #6166: Fix regression in treating Defined as definedMaxime Dénès
2017-11-19[plugins] Prepare plugin API for functional handling of state.Emilio Jesus Gallego Arias
2017-11-15Fix regression in treating Defined as definedTej Chajed
2017-11-13[api] Insert miscellaneous API deprecation back to core.Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-04[api] Deprecate all legacy uses of Name.Id in core.Emilio Jesus Gallego Arias
2017-11-01Fix FIXME: use OCaml 4.02 generative functors when available.Gaëtan Gilbert
2017-10-17[stm] Remove state-handling from Futures.Emilio Jesus Gallego Arias
2017-10-17[stm] Move interpretation state to VernacentriesEmilio Jesus Gallego Arias
2017-10-17[stm] Remove VtBack from public classification.Emilio Jesus Gallego Arias
2017-10-17[stm] First step to move interpretation of Undo commands out of the classifier.Emilio Jesus Gallego Arias
2017-10-13Merge PR #1103: Take Suggest Proof Using outside the kernel.Maxime Dénès
2017-10-11[stm] [toplevel] Move delicate state initialization to the STM (BZ#5556)Emilio Jesus Gallego Arias
2017-10-10Stm.get_hint_ctx: remove unused Str.splitGaëtan Gilbert
2017-10-06[stm] Switch to a functional APIEmilio Jesus Gallego Arias
2017-10-06[stm] [flags] Move document mode flags to the STM.Emilio Jesus Gallego Arias
2017-10-04Merge PR #1096: [stm] Warn about costly Undo operations in batch mode [BZ#5677]Maxime Dénès
2017-10-03Merge PR #1105: [stm] Remove unused "Proof using" data in `Sync` tags.Maxime Dénès
2017-10-03Merge PR #1019: Fix BZ#5655 by avoiding the creation of a cleaner thread for ...Maxime Dénès
2017-09-29[vernac] Remove `Qed exporting` syntax.Emilio Jesus Gallego Arias
2017-09-27[stm] Warn about costly Undo operations in batch mode [BZ#5677]Emilio Jesus Gallego Arias
2017-09-27[stm] Remove unused "Proof using" data in `Sync` tags.Emilio Jesus Gallego Arias
2017-09-19Remove STM vernaculars.Maxime Dénès
2017-09-19Add XML protocol support for Wait.Maxime Dénès
2017-09-11In stm, fixing a typo about flushing debugging messages.Hugo Herbelin
2017-09-07Fix BZ#5655 by avoiding the creation of a cleaner thread for empty queues.Maxime Dénès
2017-08-01Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options.Maxime Dénès
2017-07-27[toplevel] Remove long ago deprecated and NOOP options.Emilio Jesus Gallego Arias
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-13Removing a use of AUContext.instance in the STM.Pierre-Marie Pédrot
2017-07-13Safer API for Global.body_of_constant and variants.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-23Merge PR#821: [vernac] Remove stale bool parameter from `VernacStartTheoremPr...Maxime Dénès
2017-06-23Merge PR#815: STM: par: report no error to UIs in non-solve modeMaxime Dénès
2017-06-21[vernac] Remove stale bool parameter from `VernacStartTheoremProof`Emilio Jesus Gallego Arias
2017-06-20[stm] Fix route setting on VtQueryEmilio Jesus Gallego Arias
2017-06-20STM: par: report no error to UIs in non-solve modeEnrico Tassi
2017-06-20Merge PR#774: [ide] Add route_id parameter to query call.Maxime Dénès
2017-06-18[ide] Add route_id parameter to query call.Emilio Jesus Gallego Arias
2017-06-16Fix bugs and add an option for cumulativityAmin Timany
2017-06-15Merge PR#748: [stm] More fixes for nested commands [bugzilla 5589]Maxime Dénès
2017-06-11[proof] Deprecate redundant wrappers.Emilio Jesus Gallego Arias
2017-06-07[stm] More fixes for nested commands [bugzilla 5589]Emilio Jesus Gallego Arias
2017-06-07Merge PR#717: [proof] Deprecate "proof mode" APIMaxime Dénès
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-06-06Merge PR#716: Don't double up on periods in anomaliesMaxime Dénès
2017-06-03[stm] Solve bug 5577 "STM branch name is incorrect with Time"Emilio Jesus Gallego Arias
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross