aboutsummaryrefslogtreecommitdiff
path: root/stm/stm.ml
AgeCommit message (Expand)Author
2018-10-15Correct some spelling errorsBenjamin Barenblat
2018-09-24[engine] Remove and deprecate `nf_enter` et al.Emilio Jesus Gallego Arias
2018-09-17Ensure_prev_proof returns a proof that has underlying differences fromJim Fehrle
2018-07-31Code to handle "Back" command for diffs.Jim Fehrle
2018-07-07Introduce a Pcoq.Entry module for functions that ought to be exported.Pierre-Marie Pédrot
2018-06-18Remove reference name type.Maxime Dénès
2018-05-27[api] Make `vernac/` self-contained.Emilio Jesus Gallego Arias
2018-05-23[api] Move `opacity_flag` to `Proof_global`.Emilio Jesus Gallego Arias
2018-05-21[stm] Make toplevels standalone executables.Emilio Jesus Gallego Arias
2018-05-17[STM] Nested Proofs Allowed has to be executed immediatelyEnrico Tassi
2018-05-17Remove deprecation warning for nested proofs.Théo Zimmermann
2018-05-17Introduce an option to allow nested lemma, and turn it off by default.Théo Zimmermann
2018-05-01[api] Move bullets and goals selectors to `proofs/`Emilio Jesus Gallego Arias
2018-04-18Merge PR #7281: [stm] push functional API furtherEmilio Jesus Gallego Arias
2018-04-17[stm] push functional API furtherEnrico Tassi
2018-04-17[stm] expose restore/backup since ~doc is (still) dummyEnrico Tassi
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-04-11[warnings] Remove `set_current_loc` hack.Emilio Jesus Gallego Arias
2018-04-01[stm] More cleanup of "classification is not an interpreter"Emilio Jesus Gallego Arias
2018-04-01[stm] Move VernacBacktrack to the toplevel.Emilio Jesus Gallego Arias
2018-03-27stm: don't propagate side effects when editing a proofEnrico Tassi
2018-03-26Merge PR #6970: [vernac] Move `Quit` and `Drop` to the toplevel layer.Enrico Tassi
2018-03-11[vernac] Move `Quit` and `Drop` to the toplevel layer.Emilio Jesus Gallego Arias
2018-03-11[stm] Never consider `Backtrack` as part of the script.Emilio Jesus Gallego Arias
2018-03-09[located] Push inner locations in `reference` to a CAst.t node.Emilio Jesus Gallego Arias
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-03-06Deprecate UState aliases in Evd.Gaëtan Gilbert
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-02[stm] Partial fix for bug #6884 [location missing from replay nodes]Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2018-02-15[toplevel] Make toplevel state into a record.Emilio Jesus Gallego Arias
2018-02-09[error] Replace msg_error by a proper exception.Emilio Jesus Gallego Arias
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-08[vernac] vernac_expr no longer recursiveVincent Laporte
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-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[summary] Adapt STM to the new Summary API.Emilio Jesus Gallego Arias
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 08:09:35 +0000