aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Removing "exact" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* Removing "intro" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* Removing "double induction" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* Merge remote-tracking branch 'github/pr/159' into trunkGravatar Maxime Dénès2016-06-03
|\
* | Fix build of documentation (broken for four months).Gravatar Guillaume Melquiond2016-06-03
* | Merge branch 'v8.5' into trunkGravatar Guillaume Melquiond2016-06-03
|\ \
| * | Fix proof terminators not being detected in presence of curly brackets (bug #...Gravatar Guillaume Melquiond2016-06-03
| * | Make "coqdoc -g --parse-comments" behave properly (bug #4773).Gravatar Guillaume Melquiond2016-06-03
* | | Please never mention .mli-only file in *.mllib (or future *.mlpack)Gravatar Pierre Letouzey2016-06-02
* | | Move XML serialization to ide/ folder.Gravatar Pierre-Marie Pédrot2016-06-02
|\ \ \
| * | | Move ide serialization libraries from lib/ to ide/Gravatar Emilio Jesus Gallego Arias2016-06-02
| * | | Encapsulate xml serialization in xmlprotocol.mliGravatar Emilio Jesus Gallego Arias2016-06-02
| * | | Move serialization functions out of StmGravatar Emilio Jesus Gallego Arias2016-06-02
|/ / /
| * | Fix build (use the same mllib file as in trunk).Gravatar Guillaume Melquiond2016-06-02
| * | Avoid refreshing the segment widget each time a sentence is added.Gravatar Lionel Rieg2016-06-02
* | | Fix bug #4768.Gravatar Guillaume Melquiond2016-06-02
|\ \ \
* | | | Makefile.build: clean a bit the way MacOS binaries are signedGravatar Pierre Letouzey2016-06-02
| * | | Avoid refreshing the segment widget each time a sentence is added.Gravatar Lionel Rieg2016-06-02
|/ / /
* | | A slight phase of documentation and uniformization of names ofGravatar Hugo Herbelin2016-06-02
* | | Makefile.common: update PRIVATEBINARIES to repair the build on MACOSGravatar Pierre Letouzey2016-06-02
* | | coqtop: Add ltac/ to search path.Gravatar Matthieu Sozeau2016-06-02
* | | Removing pointless field NPatVar. It does not make sense to have MetaGravatar Hugo Herbelin2016-06-02
* | | Update primitive coinductive test-suite.Gravatar Matthieu Sozeau2016-06-02
* | | Add a synonymous Set Debug Ltac for Set Ltac Debug, for uniformity.Gravatar Hugo Herbelin2016-06-02
* | | Add a synonymous Set Debug Typeclasses for Set Typeclasses Debug, for uniform...Gravatar Hugo Herbelin2016-06-02
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-01
|\| |
* | | Makefile.build : follow-up of previous commitGravatar Pierre Letouzey2016-06-01
* | | Makefile.build : improved rules about .cm(x)aGravatar Pierre Letouzey2016-06-01
* | | Makefile.build : update the otags ruleGravatar Pierre Letouzey2016-06-01
* | | g_tactics : remove opt_bindings (2-line dead code)Gravatar Pierre Letouzey2016-06-01
* | | Makefile.common : avoid warnings about files linked twiceGravatar Pierre Letouzey2016-06-01
* | | Merge branch 'yet-another-makefile-bigbang' into trunkGravatar Pierre Letouzey2016-06-01
|\ \ \
| * | | Yet another Makefile reform : a unique phase without nasty make tricksGravatar Pierre Letouzey2016-06-01
| * | | Makefile: restore the use of coqdep_boot for creating .v.d filesGravatar Pierre Letouzey2016-06-01
| | * | Fix potential race condition in vm_compute.Gravatar Guillaume Melquiond2016-05-31
* | | | This patch splits pretty printing representation from IO operations.Gravatar Pierre-Marie Pédrot2016-05-31
|\ \ \ \ | |/ / / |/| | |
| | * | Revert "Rename Lexer -> CLexer."Gravatar Pierre-Marie Pédrot2016-05-31
* | | | Making the grammar/ folder independent from the other ones.Gravatar Pierre-Marie Pédrot2016-05-31
| * | | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
|/ / /
* | | Checker: avoid using obsolete names from NamesGravatar Pierre Letouzey2016-05-31
* | | Checker: no more -I kernel via a few symlinks (for Names and Esubst)Gravatar Pierre Letouzey2016-05-31
| * | Extraction : add a location in the error message about polypropGravatar Pierre Letouzey2016-05-30
* | | Extraction : add a location in the error message about polypropGravatar Pierre Letouzey2016-05-30
| * | Fix bug #4746: Anomaly: Evar ?X10 was not declared.Gravatar Pierre-Marie Pédrot2016-05-29
| * | STM: fix argument filtering for slavesGravatar Enrico Tassi2016-05-27
| * | Pfedit.get_current_context refinement (fix #4523)Gravatar Matthieu Sozeau2016-05-26
| * | rewrite/Univs: Fix bug # 4498.Gravatar Matthieu Sozeau2016-05-26
* | | Update required OCaml version in configure.Gravatar Maxime Dénès2016-05-26
| * | Extraction/Projections: Fix bug #4710Gravatar Matthieu Sozeau2016-05-23
| * | Hints/Univs: fix bug #4628 anomaliesGravatar Matthieu Sozeau2016-05-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 15:27:44 +0000