aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Remove tabulation support from pretty-printing.Gravatar Guillaume Melquiond2016-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
* | typosGravatar Enrico Tassi2016-05-23
| * Disable memoization rather than failing when files cannot be opened.Gravatar Guillaume Melquiond2016-05-20
* | Extraction: code cleanup in CommonGravatar Pierre Letouzey2016-05-20
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-20
|\|
| * native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Gravatar Pierre Letouzey2016-05-19
| * Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Gravatar Pierre Letouzey2016-05-19
* | native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Gravatar Pierre Letouzey2016-05-19
* | Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Gravatar Pierre Letouzey2016-05-19
| * adding "user-contrib" directory to ".gitignore"Gravatar Matej Kosik2016-05-19
| * Unicode.ascii_of_ident is now truly injectiveGravatar Pierre Letouzey2016-05-19
* | Unicode.ascii_of_ident is now truly injectiveGravatar Pierre Letouzey2016-05-19
* | Micromega: qualify Coq.micromega.Tauto (avoid coqdep warnings about new Init/...Gravatar Pierre Letouzey2016-05-19
* | Putting all the tactics exported by the Tactics module in the new monad API.Gravatar Pierre-Marie Pédrot2016-05-17
|\ \
| * | Removing some compatibility layers in Tactics.Gravatar Pierre-Marie Pédrot2016-05-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 05:47:47 +0000