aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\
| * Merge PR#489: [travis] Add VSTGravatar Maxime Dénès2017-03-24
| |\
| | * [travis] Add VSTGravatar Emilio Jesus Gallego Arias2017-03-24
| * | Merge PR#392: strengthened the statement of JMeq_eq_depGravatar Maxime Dénès2017-03-24
| |\ \
| * \ \ Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-24
| |\ \ \
| | * \ \ Merge PR#476: [future] Be eager when "chaining" already resolved future values.Gravatar Maxime Dénès2017-03-24
| | |\ \ \
| | * \ \ \ Merge PR#475: Opaque side effectsGravatar Maxime Dénès2017-03-24
| | |\ \ \ \
| * | \ \ \ \ Merge PR#504: [META] add support for ide librariesGravatar Maxime Dénès2017-03-24
| |\ \ \ \ \ \
| * \ \ \ \ \ \ Merge PR#503: make check not CoqIDE-specificGravatar Maxime Dénès2017-03-23
| |\ \ \ \ \ \ \
| * \ \ \ \ \ \ \ Merge PR#433: doc: fix a French-ismGravatar Maxime Dénès2017-03-23
| |\ \ \ \ \ \ \ \ | | |_|_|_|_|_|_|/ | |/| | | | | | |
| * | | | | | | | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-23
| |\ \ \ \ \ \ \ \ | | | |_|_|/ / / / | | |/| | | | | |
| | * | | | | | | Merge PR#507: Intern names bound in match patternsGravatar Maxime Dénès2017-03-23
| | |\ \ \ \ \ \ \
| | | | | | | * | | Documenting the API of side-effects.Gravatar Pierre-Marie Pédrot2017-03-23
| | | | | | | * | | Using a dedicated datastructure for side effect ordering.Gravatar Pierre-Marie Pédrot2017-03-23
| | | | | | | * | | Making the side_effects type opaque.Gravatar Pierre-Marie Pédrot2017-03-23
| | | |_|_|_|/ / / | | |/| | | | | |
| | | * | | | | | Intern names bound in match patternsGravatar Tej Chajed2017-03-23
| * | | | | | | | Merge PR#501: [travis] Fix iris-coq build.Gravatar Maxime Dénès2017-03-23
| |\ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-23
| |\ \ \ \ \ \ \ \ \ | | | |/ / / / / / / | | |/| | | | | | |
| | * | | | | | | | Merge PR#497: [travis] [8.6.only] Backport latest changes from trunk.Gravatar Maxime Dénès2017-03-23
| | |\ \ \ \ \ \ \ \
| * | | | | | | | | | Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220."Gravatar Maxime Dénès2017-03-23
| * | | | | | | | | | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-23
| |\| | | | | | | | |
| | * | | | | | | | | Merge PR#495: funind: Ignore missing info for current functionGravatar Maxime Dénès2017-03-23
| | |\ \ \ \ \ \ \ \ \ | | | |_|_|/ / / / / / | | |/| | | | | | | |
| | * | | | | | | | | Add empty Extraction.v and FunInd.v to prepare landing of PR#220.Gravatar Maxime Dénès2017-03-23
| | * | | | | | | | | Merge PR#491: Do not typecheck twice the type of opaque constants.Gravatar Maxime Dénès2017-03-23
| | |\ \ \ \ \ \ \ \ \
| | | | | | | | | * | | [META] add support for ide librariesGravatar Emilio Jesus Gallego Arias2017-03-23
| | * | | | | | | | | | Merge PR#480: show unused intro pattern warningGravatar Maxime Dénès2017-03-22
| | |\ \ \ \ \ \ \ \ \ \
| * | \ \ \ \ \ \ \ \ \ \ Merge PR#493: [safe-string] update dev/doc/changesGravatar Maxime Dénès2017-03-22
| |\ \ \ \ \ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ \ \ \ \ Merge PR#415: Use a compact representation for real literalsGravatar Maxime Dénès2017-03-22
| |\ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | * | | | make check not CoqIDE-specificGravatar Paul Steckler2017-03-22
| | | | | | | | | | | |/ / /
| * | | | | | | | | | / / / Better compatibility of TACTIC EXTEND AT LEVEL with versions of camlp5.Gravatar Hugo Herbelin2017-03-22
| | |_|_|_|_|_|_|_|_|/ / / | |/| | | | | | | | | | |
| | | | | | | | | * | | | [travis] Fix iris-coq build.Gravatar Emilio Jesus Gallego Arias2017-03-22
| | |_|_|_|_|_|_|/ / / / | |/| | | | | | | | | |
| | * | | | | | | | | | Document the changes to IZR.Gravatar Guillaume Melquiond2017-03-22
| | * | | | | | | | | | Make IZR a morphism for field.Gravatar Guillaume Melquiond2017-03-22
| | * | | | | | | | | | Mark ring morphisms as opaque.Gravatar Guillaume Melquiond2017-03-22
| | * | | | | | | | | | Change the parser and printer so that they use IZR for real constants.Gravatar Guillaume Melquiond2017-03-22
| | | | | | | | * | | | [travis] [8.6.only] Backport latest changes from trunk.Gravatar Emilio Jesus Gallego Arias2017-03-22
| | | | | |_|_|/ / / / | | | | |/| | | | | |
| | * | | | | | | | | Make IZR use a compact representation of integers.Gravatar Guillaume Melquiond2017-03-22
| | * | | | | | | | | Fix broken evaluation strategies for ring and field.Gravatar Guillaume Melquiond2017-03-22
| | * | | | | | | | | Fix some typos.Gravatar Guillaume Melquiond2017-03-22
| | * | | | | | | | | Simplify some proofs using ring and field.Gravatar Guillaume Melquiond2017-03-22
| | * | | | | | | | | Remove duplicate lemmas.Gravatar Guillaume Melquiond2017-03-22
| |/ / / / / / / / /
| | | | | | * / / / funind: Ignore missing info for current functionGravatar Tej Chajed2017-03-22
| | | | |_|/ / / / | | | |/| | | | |
| * | | | | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-03-22
| |\ \ \ \ \ \ \ \ | | | |/ / / / / / | | |/| | | | | |
| * | | | | | | | Merge PR#390: Updates to the Pretty Printing InfrastructureGravatar Maxime Dénès2017-03-22
| |\ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ Merge PR#478: Small optimization on handling of library state.Gravatar Maxime Dénès2017-03-22
| |\ \ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ \ Merge PR#482: [toplevel] Remove unusable option -notopGravatar Maxime Dénès2017-03-22
| |\ \ \ \ \ \ \ \ \ \
| | | | | | | | * | | | Add a few comments in term_typing.ml.Gravatar Maxime Dénès2017-03-21
| | | | | | | | * | | | Do not typecheck twice the type of opaque constants.Gravatar Maxime Dénès2017-03-21
| | | | | | |_|/ / / / | | | | | |/| | | | |
| | | | * | | | | | | [ide protocol] Add comment about leftover parameter.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | * | | | | | | [pp] Hide the internal representation of `std_ppcmds`.Gravatar Emilio Jesus Gallego Arias2017-03-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-23 19:39:37 +0000