aboutsummaryrefslogtreecommitdiff
path: root/stm
AgeCommit message (Expand)Author
2018-02-06Merge PR #6671: [stm] [toplevel] Make loadpath a parameter of the document.Maxime Dénès
2018-02-05Merge PR #6653: [vernac] Remove VernacGoal, allow anonymous definitions in Ve...Maxime Dénès
2018-02-05[stm] [toplevel] Make loadpath a parameter of the document.Emilio Jesus Gallego Arias
2018-02-01[vernac] Mutual theorems (VernacStartTheoremProof) always have namesVincent Laporte
2018-02-01[vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinitionVincent Laporte
2018-01-31[stm] Move options to a per-document record.Emilio Jesus Gallego Arias
2018-01-16Merge PR #6499: [vernac] Move the flags/attributes out of vernac_exprMaxime Dénès
2018-01-08[vernac] vernac_expr no longer recursiveVincent Laporte
2018-01-01Fix mli-doc issue #6531Tony Beta Lambda
2017-12-23[flags] Move global time flag into an attribute.Emilio Jesus Gallego Arias
2017-12-22Merge PR #6318: Separate vernac controls and regular commands.Maxime Dénès
2017-12-20Separate vernac controls and regular commands.Maxime Dénès
2017-12-16[stm] [ide protocol] Allow to include several commands on query.Emilio Jesus Gallego Arias
2017-12-13Merge PR #1108: [stm] Reorganize flagsMaxime Dénès
2017-12-12Merge PR #6275: [summary] Allow typed projections from global state.Maxime Dénès
2017-12-11[flags] [stm] Reorganize flags.Emilio Jesus Gallego Arias
2017-12-11[stm] Move process_id to Spawned.Emilio Jesus Gallego Arias
2017-12-09[stm] Remove all but one use of VtUnknown.Emilio Jesus Gallego Arias
2017-12-09[summary] Adapt STM to the new Summary API.Emilio Jesus Gallego Arias
2017-12-01Proper nametab handling of global universe namesMatthieu Sozeau
2017-12-01Merge PR #6233: [proof] [api] Rename proof types in preparation for functiona...Maxime Dénès
2017-11-29Remove "obsolete_locality" and fix STM vernac classification.Maxime Dénès
2017-11-29[proof] [api] Rename proof types in preparation for functionalization.Emilio Jesus Gallego Arias
2017-11-27[vernac] Adjust `interp` to pass polymorphic in the attributes.Emilio Jesus Gallego Arias
2017-11-27Merge PR #6207: [stm] Allow delayed constant in interactive mode.Maxime Dénès
2017-11-23Merge PR #1092: [stm] [doc] Add some documentation to obscure AsyncTaskQueueMaxime Dénès
2017-11-21[stm] [doc] Add some documentation to AsyncTaskQueue APIEmilio Jesus Gallego Arias
2017-11-21[printing] Deprecate all printing functions accessing the global proof.Emilio Jesus Gallego Arias
2017-11-21[stm] Allow delayed constant in interactive mode.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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:38:08 +0000