aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Two protections against failures when printing evar_map.Gravatar Hugo Herbelin2016-08-17
* Fixing printing in debugger (no global env in debugger).Gravatar Hugo Herbelin2016-08-17
* A fix to dev/include.Gravatar Hugo Herbelin2016-08-17
* Removing dead unsafe debugging code in Constrintern.Gravatar Pierre-Marie Pédrot2016-08-16
* Merge PR #250 into v8.6Gravatar Pierre-Marie Pédrot2016-08-16
|\
* \ Merge PR #237 into v8.6Gravatar Pierre-Marie Pédrot2016-08-16
|\ \
* \ \ Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-16
|\ \ \
* \ \ \ Efficiently generate the pretyping contexts.Gravatar Pierre-Marie Pédrot2016-08-16
|\ \ \ \
| | * \ \ Merge branch 'pr255' into v8.5 (bug #5015)Gravatar Guillaume Melquiond2016-08-16
| | |\ \ \
| | | * | | Fix regression in Coqide's "forward one command" commandGravatar Xavier Leroy2016-08-14
| | |/ / /
| | * | | Do not assume the "TERM" environment variable is always set (bug #5007).Gravatar Guillaume Melquiond2016-08-11
| | * | | Use the "md5" command on OpenBSD (bug #5008).Gravatar Guillaume Melquiond2016-08-11
* | | | | Make code a bit clearer by removing optional argument.Gravatar Guillaume Melquiond2016-08-10
* | | | | Remove unused optional "predicative" argument.Gravatar Guillaume Melquiond2016-08-10
* | | | | Make it a bit more obvious when variables are of type unit.Gravatar Guillaume Melquiond2016-08-10
* | | | | Reduce warning noise when compiling the standard library.Gravatar Guillaume Melquiond2016-08-09
* | | | | Make List.map_filter(_i) tail-recursive.Gravatar Guillaume Melquiond2016-08-09
| | * | | Fix #5000: Document the native compiler soundness bug due to Unicode mangling.Gravatar Pierre-Marie Pédrot2016-08-07
| * | | | Using a dedicated kind of substitutions in evar name generation.Gravatar Pierre-Marie Pédrot2016-08-06
| * | | | Using the extended contexts in pretyping.Gravatar Pierre-Marie Pédrot2016-08-05
| * | | | Use sets instead of lists for names to avoid in evar generation.Gravatar Pierre-Marie Pédrot2016-08-04
| * | | | Simplifying code in evar generation.Gravatar Pierre-Marie Pédrot2016-08-04
| * | | | Exporting the renaming API for evar declaration.Gravatar Pierre-Marie Pédrot2016-08-04
| * | | | Embedding the pretyping environment in a dummy record.Gravatar Pierre-Marie Pédrot2016-08-04
|/ / / /
| * | | Fix documentation typo (bug #4994).Gravatar Guillaume Melquiond2016-08-04
| * | | Fix bug #4673: regression in setoid_rewrite.Gravatar Matthieu Sozeau2016-07-29
* | | | Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-07-29
|\| | |
| * | | Update CHANGES about #3886 bugfixGravatar Matthieu Sozeau2016-07-29
| * | | Fix bug #3886, generation of obligations of fixesGravatar Matthieu Sozeau2016-07-29
| * | | Fix #4769, univ poly and elim schemes in sectionsGravatar Matthieu Sozeau2016-07-29
* | | | COMMENT: moving misplaced comment where it belongsGravatar Matej Kosik2016-07-29
* | | | Adding a flag in CoqIDE to configure UNIX/Windows line ending.Gravatar Pierre-Marie Pédrot2016-07-26
* | | | restore compatibility with gallium's camlp4 (broken by commit 8e07227c)Gravatar Pierre Letouzey2016-07-26
| * | | Update CHANGES about critical bugfix and othersGravatar Matthieu Sozeau2016-07-26
| * | | Merge branch 'bug4754' into v8.5Gravatar Matthieu Sozeau2016-07-26
| |\ \ \
| | * | | Fix bug #4754, allow conversion problems to remainGravatar Matthieu Sozeau2016-07-26
| |/ / /
* | | | Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-07-26
|\| | |
| * | | Merge branch 'bug4876' into v8.5Gravatar Matthieu Sozeau2016-07-26
| |\ \ \
* | \ \ \ Merge remote-tracking branch 'github/bug4679' into v8.6Gravatar Matthieu Sozeau2016-07-25
|\ \ \ \ \
| | | * | | Fix bug #4876: critical bug in guard condition checker.Gravatar Matthieu Sozeau2016-07-25
| | |/ / /
| * | | | Fix bug #4679, weakened setoid_rewrite unificationGravatar Matthieu Sozeau2016-07-21
* | | | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-20
|\ \ \ \ \ | |/ / / / |/| / / / | |/ / /
| * | | Update CHANGESGravatar Matthieu Sozeau2016-07-20
| * | | Fix bug #4780: universe leak in letin_tacGravatar Matthieu Sozeau2016-07-20
* | | | Update CHANGESGravatar Matthieu Sozeau2016-07-20
* | | | Fix bug #4780: universe leak in letin_tacGravatar Matthieu Sozeau2016-07-20
| | | * Allow `STDTIME=foo make`Gravatar Jason Gross2016-07-19
| |_|/ |/| |
| * | Fix Errors.out missing a dot...Gravatar Matthieu Sozeau2016-07-19
* | | Complementing previous commit on fixes for printing binding patterns.Gravatar Hugo Herbelin2016-07-19
* | | Some extra fixes in printing patterns in binders.Gravatar Hugo Herbelin2016-07-19