aboutsummaryrefslogtreecommitdiff
path: root/stm
AgeCommit message (Expand)Author
2018-11-17[vernacextend] Consolidate extension points APIEmilio Jesus Gallego Arias
2018-11-15Move generating library dirpath to stm in compile mode.Gaëtan Gilbert
2018-11-15coqide: use correct toplevel name in filesGaëtan Gilbert
2018-11-13[vernac] Rename Vernacinterp to Vernacextend and move extension functions there.Emilio Jesus Gallego Arias
2018-11-05Merge PR #8515: Command driven attributesPierre-Marie Pédrot
2018-11-02Universe Polymorphism is a normal attribute modulo the stm (no Flags)Gaëtan Gilbert
2018-11-02Add comment in stm to unsupport attributes for special commandsGaëtan Gilbert
2018-11-02Make attributes more general to make defining #[universes(...)] easyGaëtan Gilbert
2018-11-02Command driven attributes.Gaëtan Gilbert
2018-11-02{Vernacentries -> Attributes}.attributes_of_flagsGaëtan Gilbert
2018-11-02Move attributes out of vernacinterp to new attributes moduleGaëtan Gilbert
2018-10-30Move abstract out of tactics.mlGaëtan Gilbert
2018-10-15Correct some spelling errorsBenjamin Barenblat
2018-10-03Rename CEphemeron.clear→clean for clarity.whitequark
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-09-10Adding a command "Declare Scope" and deprecating scope implicit declaration.Hugo Herbelin
2018-09-05[build] Preliminary support for building Coq with `dune`.Emilio Jesus Gallego Arias
2018-08-14Remove unneeded file: workerLoop.ml/.mli were moved to toplevel in commit 382...Jim Fehrle
2018-07-31Code to handle "Back" command for diffs.Jim Fehrle
2018-07-29Classify "Declare Custom" as VtNow for the stm.Hugo Herbelin
2018-07-29Adding support for custom entries in notations.Hugo Herbelin
2018-07-12Export a wrapper simplifying the registration of vernacular commands.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:03:34 +0000