aboutsummaryrefslogtreecommitdiff
path: root/stm
AgeCommit message (Expand)Author
2018-07-11Merge PR #7898: Remove camlp4 remainsEmilio Jesus Gallego Arias
2018-07-07Introduce a Pcoq.Entry module for functions that ought to be exported.Pierre-Marie Pédrot
2018-07-03[vernac] mk_atts: an atts record with default valuesVincent Laporte
2018-07-03[vernac] attribute_of_flagsVincent Laporte
2018-06-18Remove reference name type.Maxime Dénès
2018-06-15[spawn] don't create a control socket on Unix (Fix #7713)Enrico Tassi
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-22Merge PR #7384: Split UniversesPierre-Marie Pédrot
2018-05-21[ide] Remove special option `-ideslave`Emilio Jesus Gallego Arias
2018-05-21[stm] Make toplevels standalone executables.Emilio Jesus Gallego Arias
2018-05-17Split off Universes functions dealing with generating new universes.Gaëtan Gilbert
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-19Merge PR #7282: [toplevel] allow toploop_init change Coq optionsEmilio Jesus Gallego Arias
2018-04-19[toplevel] let toploop_init change Coq optionsEnrico Tassi
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-05Merge PR #7139: [stm] More cleanup of "classification is not an interpreter"Enrico Tassi
2018-04-04Merge PR #7138: [stm] Move VernacBacktrack to the toplevel.Enrico Tassi
2018-04-01Merge PR #7132: [doc] Add some more documentation to STM API.Enrico Tassi
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-31[doc] Add some more documentation to STM API.Emilio Jesus Gallego Arias
2018-03-30Remove deprecated commands Arguments Scope and Implicit ArgumentsJasper Hugunin
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-09Implement the Export Set/Unset feature.Pierre-Marie Pédrot
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-13Merge PR #6693: [toplevel] Refactor command line argument handling.Maxime Dénès
2018-02-09[error] Replace msg_error by a proper exception.Emilio Jesus Gallego Arias
2018-02-09[toplevel] Refactor command line argument handling.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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 13:48:41 +0000