aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/texmacspp.ml
Commit message (Expand)AuthorAge
* Move serialization functions out of StmGravatar Emilio Jesus Gallego Arias2016-06-02
* Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Gravatar Matthieu Sozeau2016-04-04
|\
* | Moving the Ltac definition command to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* | Moving Tactic Notation to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* | Moving VernacSolve to an EXTEND-based definition.Gravatar Pierre-Marie Pédrot2016-03-19
* | Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Gravatar Hugo Herbelin2016-03-13
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\ \
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | | CLEANUP: removing unused fieldGravatar Matej Kosik2016-01-11
* | | Remove unused functions.Gravatar Guillaume Melquiond2016-01-01
* | | CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedGravatar Matej Kosik2015-12-18
* | | CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular comma...Gravatar Matej Kosik2015-12-18
* | | CLEANUP: Vernacexpr.vernac_exprGravatar Matej Kosik2015-12-18
|/ /
* | Axioms now support the universe binding syntax.Gravatar Pierre-Marie Pédrot2015-10-08
* | Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
| * Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080Gravatar Jason Gross2015-08-14
|/
* Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Gravatar Lionel Rieg2015-06-26
* Add a [Redirect] vernacular commandGravatar Clément Pit--Claudel2015-05-04
* Fix some typos.Gravatar Guillaume Melquiond2015-04-02
* Putting the From parameter of the Require command into the AST.Gravatar Pierre-Marie Pédrot2015-03-27
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Update headers.Gravatar Maxime Dénès2015-01-12
* Proof using: New vernacular to name sets of section variablesGravatar Enrico Tassi2014-12-18
* Add additional location information to AST XMLs.Gravatar Carst Tankink2014-10-01
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* XML pretty printing for AST (work by François Poulain, project DoCoq)Gravatar Enrico Tassi2014-09-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 22:17:54 +0000