aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/stm.ml
Commit message (Expand)AuthorAge
...
* | | [printing] Deprecate all printing functions accessing the global proof.Gravatar Emilio Jesus Gallego Arias2017-11-21
|/ /
| * [stm] Allow delayed constant in interactive mode.Gravatar Emilio Jesus Gallego Arias2017-11-21
|/
* Merge PR #6183: [plugins] Prepare plugin API for functional handling of state.Gravatar Maxime Dénès2017-11-20
|\
* \ Merge PR #6166: Fix regression in treating Defined as definedGravatar Maxime Dénès2017-11-20
|\ \
| | * [plugins] Prepare plugin API for functional handling of state.Gravatar Emilio Jesus Gallego Arias2017-11-19
| |/ |/|
| * Fix regression in treating Defined as definedGravatar Tej Chajed2017-11-15
* | [api] Insert miscellaneous API deprecation back to core.Gravatar Emilio Jesus Gallego Arias2017-11-13
|/
* [api] Deprecate all legacy uses of Name.Id in core.Gravatar Emilio Jesus Gallego Arias2017-11-04
* Fix FIXME: use OCaml 4.02 generative functors when available.Gravatar Gaëtan Gilbert2017-11-01
* [stm] Remove state-handling from Futures.Gravatar Emilio Jesus Gallego Arias2017-10-17
* [stm] Move interpretation state to VernacentriesGravatar Emilio Jesus Gallego Arias2017-10-17
* [stm] Remove VtBack from public classification.Gravatar Emilio Jesus Gallego Arias2017-10-17
* [stm] First step to move interpretation of Undo commands out of the classifier.Gravatar Emilio Jesus Gallego Arias2017-10-17
* Merge PR #1103: Take Suggest Proof Using outside the kernel.Gravatar Maxime Dénès2017-10-13
|\
* | [stm] [toplevel] Move delicate state initialization to the STM (BZ#5556)Gravatar Emilio Jesus Gallego Arias2017-10-11
| * Stm.get_hint_ctx: remove unused Str.splitGravatar Gaëtan Gilbert2017-10-10
|/
* [stm] Switch to a functional APIGravatar Emilio Jesus Gallego Arias2017-10-06
* [stm] [flags] Move document mode flags to the STM.Gravatar Emilio Jesus Gallego Arias2017-10-06
* Merge PR #1096: [stm] Warn about costly Undo operations in batch mode [BZ#5677]Gravatar Maxime Dénès2017-10-04
|\
* \ Merge PR #1105: [stm] Remove unused "Proof using" data in `Sync` tags.Gravatar Maxime Dénès2017-10-03
|\ \
* | | [vernac] Remove `Qed exporting` syntax.Gravatar Emilio Jesus Gallego Arias2017-09-29
| | * [stm] Warn about costly Undo operations in batch mode [BZ#5677]Gravatar Emilio Jesus Gallego Arias2017-09-27
| |/ |/|
| * [stm] Remove unused "Proof using" data in `Sync` tags.Gravatar Emilio Jesus Gallego Arias2017-09-27
|/
* Remove STM vernaculars.Gravatar Maxime Dénès2017-09-19
* Add XML protocol support for Wait.Gravatar Maxime Dénès2017-09-19
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* Removing a use of AUContext.instance in the STM.Gravatar Pierre-Marie Pédrot2017-07-13
* Safer API for Global.body_of_constant and variants.Gravatar Pierre-Marie Pédrot2017-07-13
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Merge PR#821: [vernac] Remove stale bool parameter from `VernacStartTheoremPr...Gravatar Maxime Dénès2017-06-23
|\
* \ Merge PR#815: STM: par: report no error to UIs in non-solve modeGravatar Maxime Dénès2017-06-23
|\ \
| | * [vernac] Remove stale bool parameter from `VernacStartTheoremProof`Gravatar Emilio Jesus Gallego Arias2017-06-21
* | | [stm] Fix route setting on VtQueryGravatar Emilio Jesus Gallego Arias2017-06-20
| |/ |/|
| * STM: par: report no error to UIs in non-solve modeGravatar Enrico Tassi2017-06-20
* | [ide] Add route_id parameter to query call.Gravatar Emilio Jesus Gallego Arias2017-06-18
|/
* Merge PR#748: [stm] More fixes for nested commands [bugzilla 5589]Gravatar Maxime Dénès2017-06-15
|\
* | [proof] Deprecate redundant wrappers.Gravatar Emilio Jesus Gallego Arias2017-06-11
| * [stm] More fixes for nested commands [bugzilla 5589]Gravatar Emilio Jesus Gallego Arias2017-06-07
|/
* Merge PR#717: [proof] Deprecate "proof mode" APIGravatar Maxime Dénès2017-06-07
|\
* | Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* | Merge PR#716: Don't double up on periods in anomaliesGravatar Maxime Dénès2017-06-06
|\ \
* | | [stm] Solve bug 5577 "STM branch name is incorrect with Time"Gravatar Emilio Jesus Gallego Arias2017-06-03
| * | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
|/ /
* | [emacs] [toplevel] Make emacs flag local to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-06-01
| * [proof] Deprecate "proof mode" APIGravatar Emilio Jesus Gallego Arias2017-05-31
|/
* [stm] Rename Side-Effect type.Gravatar Emilio Jesus Gallego Arias2017-05-27
* [stm] Uniformize `Sideff / Sideff.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Merge PR#645: [stm] Tweak debug options.Gravatar Maxime Dénès2017-05-25
|\
* \ Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \
| | * [stm] Tweak debug options.Gravatar Emilio Jesus Gallego Arias2017-05-18
| |/