aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-06-04Merge remote-tracking branch 'github/pr/184' into trunkMaxime Dénès
2016-06-03Remove a few tactics from the Tacexpr AST.Pierre-Marie Pédrot
2016-06-03Removing "rename" from the tactic AST.Pierre-Marie Pédrot
2016-06-03Removing "exact" from the tactic AST.Pierre-Marie Pédrot
2016-06-03Removing "intro" from the tactic AST.Pierre-Marie Pédrot
2016-06-03Removing "double induction" from the tactic AST.Pierre-Marie Pédrot
2016-06-03Merge remote-tracking branch 'github/pr/159' into trunkMaxime Dénès
2016-06-03Fix build of documentation (broken for four months).Guillaume Melquiond
2016-06-03Merge branch 'v8.5' into trunkGuillaume Melquiond
2016-06-03Fix proof terminators not being detected in presence of curly brackets (bug #...Guillaume Melquiond
2016-06-03Make "coqdoc -g --parse-comments" behave properly (bug #4773).Guillaume Melquiond
2016-06-02Please never mention .mli-only file in *.mllib (or future *.mlpack)Pierre Letouzey
2016-06-02Add documentation to the low-level `Pp` functions.Emilio Jesus Gallego Arias
2016-06-02Move XML serialization to ide/ folder.Pierre-Marie Pédrot
2016-06-02Move ide serialization libraries from lib/ to ide/Emilio Jesus Gallego Arias
2016-06-02Encapsulate xml serialization in xmlprotocol.mliEmilio Jesus Gallego Arias
2016-06-02Move serialization functions out of StmEmilio Jesus Gallego Arias
2016-06-02Fix build (use the same mllib file as in trunk).Guillaume Melquiond
2016-06-02Avoid refreshing the segment widget each time a sentence is added.Lionel Rieg
2016-06-02Fix bug #4768.Guillaume Melquiond
2016-06-02Makefile.build: clean a bit the way MacOS binaries are signedPierre Letouzey
2016-06-02Avoid refreshing the segment widget each time a sentence is added.Lionel Rieg
2016-06-02A slight phase of documentation and uniformization of names ofHugo Herbelin
2016-06-02Makefile.common: update PRIVATEBINARIES to repair the build on MACOSPierre Letouzey
2016-06-02coqtop: Add ltac/ to search path.Matthieu Sozeau
2016-06-02Removing pointless field NPatVar. It does not make sense to have MetaHugo Herbelin
2016-06-02Update primitive coinductive test-suite.Matthieu Sozeau
2016-06-02Add a synonymous Set Debug Ltac for Set Ltac Debug, for uniformity.Hugo Herbelin
2016-06-02Add a synonymous Set Debug Typeclasses for Set Typeclasses Debug, for uniform...Hugo Herbelin
2016-06-01Merge branch 'v8.5'Pierre-Marie Pédrot
2016-06-01Makefile.build : follow-up of previous commitPierre Letouzey
2016-06-01Makefile.build : improved rules about .cm(x)aPierre Letouzey
2016-06-01Makefile.build : update the otags rulePierre Letouzey
2016-06-01g_tactics : remove opt_bindings (2-line dead code)Pierre Letouzey
2016-06-01Makefile.common : avoid warnings about files linked twicePierre Letouzey
2016-06-01Merge branch 'yet-another-makefile-bigbang' into trunkPierre Letouzey
2016-06-01Yet another Makefile reform : a unique phase without nasty make tricksPierre Letouzey
2016-06-01Makefile: restore the use of coqdep_boot for creating .v.d filesPierre Letouzey
2016-05-31Fix potential race condition in vm_compute.Guillaume Melquiond
2016-05-31This patch splits pretty printing representation from IO operations.Pierre-Marie Pédrot
2016-05-31Revert "Rename Lexer -> CLexer."Pierre-Marie Pédrot
2016-05-31Making the grammar/ folder independent from the other ones.Pierre-Marie Pédrot
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-31Checker: avoid using obsolete names from NamesPierre Letouzey
2016-05-31Checker: no more -I kernel via a few symlinks (for Names and Esubst)Pierre Letouzey
2016-05-30Extraction : add a location in the error message about polypropPierre Letouzey
2016-05-30Extraction : add a location in the error message about polypropPierre Letouzey
2016-05-29Fix bug #4746: Anomaly: Evar ?X10 was not declared.Pierre-Marie Pédrot
2016-05-27STM: fix argument filtering for slavesEnrico Tassi
2016-05-26Pfedit.get_current_context refinement (fix #4523)Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-04 18:38:04 +0000