aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
Commit message (Expand)AuthorAge
* [api] Make `vernac/` self-contained.Gravatar Emilio Jesus Gallego Arias2018-05-27
* [api] Move `opacity_flag` to `Proof_global`.Gravatar Emilio Jesus Gallego Arias2018-05-23
* Merge PR #7384: Split UniversesGravatar Pierre-Marie Pédrot2018-05-22
|\
* | [ide] Remove special option `-ideslave`Gravatar Emilio Jesus Gallego Arias2018-05-21
* | [stm] Make toplevels standalone executables.Gravatar Emilio Jesus Gallego Arias2018-05-21
| * Split off Universes functions dealing with generating new universes.Gravatar Gaëtan Gilbert2018-05-17
|/
* [STM] Nested Proofs Allowed has to be executed immediatelyGravatar Enrico Tassi2018-05-17
* Remove deprecation warning for nested proofs.Gravatar Théo Zimmermann2018-05-17
* Introduce an option to allow nested lemma, and turn it off by default.Gravatar Théo Zimmermann2018-05-17
* [api] Move bullets and goals selectors to `proofs/`Gravatar Emilio Jesus Gallego Arias2018-05-01
* Merge PR #7282: [toplevel] allow toploop_init change Coq optionsGravatar Emilio Jesus Gallego Arias2018-04-19
|\
| * [toplevel] let toploop_init change Coq optionsGravatar Enrico Tassi2018-04-19
* | Merge PR #7281: [stm] push functional API furtherGravatar Emilio Jesus Gallego Arias2018-04-18
|\ \
| * | [stm] push functional API furtherGravatar Enrico Tassi2018-04-17
| |/
* / [stm] expose restore/backup since ~doc is (still) dummyGravatar Enrico Tassi2018-04-17
|/
* Evar maps contain econstrs.Gravatar Gaëtan Gilbert2018-04-13
* [warnings] Remove `set_current_loc` hack.Gravatar Emilio Jesus Gallego Arias2018-04-11
* Merge PR #7139: [stm] More cleanup of "classification is not an interpreter"Gravatar Enrico Tassi2018-04-05
|\
* \ Merge PR #7138: [stm] Move VernacBacktrack to the toplevel.Gravatar Enrico Tassi2018-04-04
|\ \
* \ \ Merge PR #7132: [doc] Add some more documentation to STM API.Gravatar Enrico Tassi2018-04-01
|\ \ \
| | | * [stm] More cleanup of "classification is not an interpreter"Gravatar Emilio Jesus Gallego Arias2018-04-01
| | |/
| | * [stm] Move VernacBacktrack to the toplevel.Gravatar Emilio Jesus Gallego Arias2018-04-01
| * | [doc] Add some more documentation to STM API.Gravatar Emilio Jesus Gallego Arias2018-03-31
| |/
* / Remove deprecated commands Arguments Scope and Implicit ArgumentsGravatar Jasper Hugunin2018-03-30
|/
* stm: don't propagate side effects when editing a proofGravatar Enrico Tassi2018-03-27
* Merge PR #6970: [vernac] Move `Quit` and `Drop` to the toplevel layer.Gravatar Enrico Tassi2018-03-26
|\
| * [vernac] Move `Quit` and `Drop` to the toplevel layer.Gravatar Emilio Jesus Gallego Arias2018-03-11
* | [stm] Never consider `Backtrack` as part of the script.Gravatar Emilio Jesus Gallego Arias2018-03-11
|/
* [located] Push inner locations in `reference` to a CAst.t node.Gravatar Emilio Jesus Gallego Arias2018-03-09
* [located] More work towards using CAst.tGravatar Emilio Jesus Gallego Arias2018-03-09
* Implement the Export Set/Unset feature.Gravatar Pierre-Marie Pédrot2018-03-09
* Deprecate UState aliases in Evd.Gravatar Gaëtan Gilbert2018-03-06
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | [stm] Partial fix for bug #6884 [location missing from replay nodes]Gravatar Emilio Jesus Gallego Arias2018-03-02
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
* [toplevel] Make toplevel state into a record.Gravatar Emilio Jesus Gallego Arias2018-02-15
* Merge PR #6693: [toplevel] Refactor command line argument handling.Gravatar Maxime Dénès2018-02-13
|\
* | [error] Replace msg_error by a proper exception.Gravatar Emilio Jesus Gallego Arias2018-02-09
| * [toplevel] Refactor command line argument handling.Gravatar Emilio Jesus Gallego Arias2018-02-09
|/
* Merge PR #6671: [stm] [toplevel] Make loadpath a parameter of the document.Gravatar Maxime Dénès2018-02-06
|\
* \ Merge PR #6653: [vernac] Remove VernacGoal, allow anonymous definitions in Ve...Gravatar Maxime Dénès2018-02-05
|\ \
| | * [stm] [toplevel] Make loadpath a parameter of the document.Gravatar Emilio Jesus Gallego Arias2018-02-05
| |/ |/|
| * [vernac] Mutual theorems (VernacStartTheoremProof) always have namesGravatar Vincent Laporte2018-02-01
| * [vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinitionGravatar Vincent Laporte2018-02-01
* | [stm] Move options to a per-document record.Gravatar Emilio Jesus Gallego Arias2018-01-31
|/
* Merge PR #6499: [vernac] Move the flags/attributes out of vernac_exprGravatar Maxime Dénès2018-01-16
|\
| * [vernac] vernac_expr no longer recursiveGravatar Vincent Laporte2018-01-08
* | Fix mli-doc issue #6531Gravatar Tony Beta Lambda2018-01-01
|/
* [flags] Move global time flag into an attribute.Gravatar Emilio Jesus Gallego Arias2017-12-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-21 22:56:45 +0000