Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| * | | | | | | | Merge PR#475: Opaque side effects | 2017-03-24 | ||
| |\ \ \ \ \ \ \ | ||||
* | \ \ \ \ \ \ \ | Merge PR#504: [META] add support for ide libraries | 2017-03-24 | ||
|\ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ | Merge PR#503: make check not CoqIDE-specific | 2017-03-23 | ||
|\ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ | Merge PR#433: doc: fix a French-ism | 2017-03-23 | ||
|\ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | ||||
* | | | | | | | | | | | Merge branch 'v8.6' into trunk | 2017-03-23 | ||
|\ \ \ \ \ \ \ \ \ \ \ | | |_|_|/ / / / / / / | |/| | | | | | | | | | ||||
| * | | | | | | | | | | Merge PR#507: Intern names bound in match patterns | 2017-03-23 | ||
| |\ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | * | | | | | | Documenting the API of side-effects. | 2017-03-23 | ||
| | | | | | * | | | | | | Using a dedicated datastructure for side effect ordering. | 2017-03-23 | ||
| | | | | | * | | | | | | Making the side_effects type opaque. | 2017-03-23 | ||
| | |_|_|_|/ / / / / / | |/| | | | | | | | | | ||||
| | * | | | | | | | | | Intern names bound in match patterns | 2017-03-23 | ||
* | | | | | | | | | | | Merge PR#501: [travis] Fix iris-coq build. | 2017-03-23 | ||
|\ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ | Merge branch 'v8.6' into trunk | 2017-03-23 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ | | |/ / / / / / / / / / | |/| | | | | | | | | | | ||||
| * | | | | | | | | | | | Merge PR#497: [travis] [8.6.only] Backport latest changes from trunk. | 2017-03-23 | ||
| |\ \ \ \ \ \ \ \ \ \ \ | ||||
* | | | | | | | | | | | | | Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220." | 2017-03-23 | ||
* | | | | | | | | | | | | | Merge branch 'v8.6' into trunk | 2017-03-23 | ||
|\| | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | Merge PR#495: funind: Ignore missing info for current function | 2017-03-23 | ||
| |\ \ \ \ \ \ \ \ \ \ \ \ | | |_|_|/ / / / / / / / / | |/| | | | | | | | | | | | ||||
| * | | | | | | | | | | | | Add empty Extraction.v and FunInd.v to prepare landing of PR#220. | 2017-03-23 | ||
| * | | | | | | | | | | | | Merge PR#491: Do not typecheck twice the type of opaque constants. | 2017-03-23 | ||
| |\ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | * | | | | | | [META] add support for ide libraries | 2017-03-23 | ||
| * | | | | | | | | | | | | | Merge PR#480: show unused intro pattern warning | 2017-03-22 | ||
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* | \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#493: [safe-string] update dev/doc/changes | 2017-03-22 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#415: Use a compact representation for real literals | 2017-03-22 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | * | | | | | | | make check not CoqIDE-specific | 2017-03-22 | ||
| | | | | | | | | | |/ / / / / / | ||||
| | | | | | | | | | | | | | * / | [pp] Add anomaly header to anomaly error messages. | 2017-03-22 | ||
| | | | | | | | | | | |_|_|/ / | | | | | | | | | | |/| | | | | ||||
* | | | | | | | | | / | | | | | Better compatibility of TACTIC EXTEND AT LEVEL with versions of camlp5. | 2017-03-22 | ||
| |_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | ||||
| | | | | | | | * | | | | | | [travis] Fix iris-coq build. | 2017-03-22 | ||
| |_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | Document the changes to IZR. | 2017-03-22 | ||
| * | | | | | | | | | | | | Make IZR a morphism for field. | 2017-03-22 | ||
| * | | | | | | | | | | | | Mark ring morphisms as opaque. | 2017-03-22 | ||
| * | | | | | | | | | | | | Change the parser and printer so that they use IZR for real constants. | 2017-03-22 | ||
| | | | | | | * | | | | | | [travis] [8.6.only] Backport latest changes from trunk. | 2017-03-22 | ||
| | | | |_|_|/ / / / / / | | | |/| | | | | | | | | ||||
| * | | | | | | | | | | | Make IZR use a compact representation of integers. | 2017-03-22 | ||
| * | | | | | | | | | | | Fix broken evaluation strategies for ring and field. | 2017-03-22 | ||
| * | | | | | | | | | | | Fix some typos. | 2017-03-22 | ||
| * | | | | | | | | | | | Simplify some proofs using ring and field. | 2017-03-22 | ||
| * | | | | | | | | | | | Remove duplicate lemmas. | 2017-03-22 | ||
|/ / / / / / / / / / / | ||||
| | | | | * / / / / / | funind: Ignore missing info for current function | 2017-03-22 | ||
| | | |_|/ / / / / / | | |/| | | | | | | | ||||
* | | | | | | | | | | Merge branch 'v8.6' | 2017-03-22 | ||
|\ \ \ \ \ \ \ \ \ \ | | |/ / / / / / / / | |/| | | | | | | | | ||||
* | | | | | | | | | | Merge PR#390: Updates to the Pretty Printing Infrastructure | 2017-03-22 | ||
|\ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ | Merge PR#478: Small optimization on handling of library state. | 2017-03-22 | ||
|\ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR#482: [toplevel] Remove unusable option -notop | 2017-03-22 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | * | | | | | | Add a few comments in term_typing.ml. | 2017-03-21 | ||
| | | | | | | * | | | | | | Do not typecheck twice the type of opaque constants. | 2017-03-21 | ||
| | | | | |_|/ / / / / / | | | | |/| | | | | | | | ||||
| | | * | | | | | | | | | [ide protocol] Add comment about leftover parameter. | 2017-03-21 | ||
| | | * | | | | | | | | | [pp] Hide the internal representation of `std_ppcmds`. | 2017-03-21 | ||
| | | * | | | | | | | | | [pp] Fix bug in richpp Format use. | 2017-03-21 | ||
| | | * | | | | | | | | | [extraction] Flush formatters at end of output. | 2017-03-21 | ||
| | | * | | | | | | | | | [xml] Restore protocol compatibility with 8.6. | 2017-03-21 | ||
| | | * | | | | | | | | | [stm] Add common toploop for workers. | 2017-03-21 | ||
| | | * | | | | | | | | | [pp] Remove uses of expensive string_of_ppcmds. | 2017-03-21 |