aboutsummaryrefslogtreecommitdiff
path: root/stm/texmacspp.ml
AgeCommit message (Expand)Author
2016-06-02Move serialization functions out of StmEmilio Jesus Gallego Arias
2016-04-04Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Matthieu Sozeau
2016-03-20Moving the Ltac definition command to an EXTEND based command.Pierre-Marie Pédrot
2016-03-20Moving Tactic Notation to an EXTEND based command.Pierre-Marie Pédrot
2016-03-19Moving VernacSolve to an EXTEND-based definition.Pierre-Marie Pédrot
2016-03-13Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Hugo Herbelin
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: removing unused fieldMatej Kosik
2016-01-01Remove unused functions.Guillaume Melquiond
2015-12-18CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedMatej Kosik
2015-12-18CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular comma...Matej Kosik
2015-12-18CLEANUP: Vernacexpr.vernac_exprMatej Kosik
2015-10-08Axioms now support the universe binding syntax.Pierre-Marie Pédrot
2015-09-14Univs: Add universe binding lists to definitionsMatthieu Sozeau
2015-08-14Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080Jason Gross
2015-06-26Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Lionel Rieg
2015-05-04Add a [Redirect] vernacular commandClément Pit--Claudel
2015-04-02Fix some typos.Guillaume Melquiond
2015-03-27Putting the From parameter of the Require command into the AST.Pierre-Marie Pédrot
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-12-18Proof using: New vernacular to name sets of section variablesEnrico Tassi
2014-10-01Add additional location information to AST XMLs.Carst Tankink
2014-09-30Add syntax for naming new goals in refine: writing ?[id] instead of _Hugo Herbelin
2014-09-29XML pretty printing for AST (work by François Poulain, project DoCoq)Enrico Tassi