aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-03-25Mathcomp overlay.Maxime Dénès
2017-03-24Fix interpretation of Ltac patterns episode 2.Maxime Dénès
2017-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-03-24Merge PR#489: [travis] Add VSTMaxime Dénès
2017-03-24[travis] Add VSTEmilio Jesus Gallego Arias
2017-03-24Merge PR#392: strengthened the statement of JMeq_eq_depMaxime Dénès
2017-03-24Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-24Merge PR#476: [future] Be eager when "chaining" already resolved future values.Maxime Dénès
2017-03-24Merge PR#475: Opaque side effectsMaxime Dénès
2017-03-24Merge PR#504: [META] add support for ide librariesMaxime Dénès
2017-03-23Merge PR#503: make check not CoqIDE-specificMaxime Dénès
2017-03-23Merge PR#433: doc: fix a French-ismMaxime Dénès
2017-03-23Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-23Merge PR#507: Intern names bound in match patternsMaxime Dénès
2017-03-23Documenting the API of side-effects.Pierre-Marie Pédrot
2017-03-23Using a dedicated datastructure for side effect ordering.Pierre-Marie Pédrot
2017-03-23Making the side_effects type opaque.Pierre-Marie Pédrot
2017-03-23Intern names bound in match patternsTej Chajed
2017-03-23Merge PR#501: [travis] Fix iris-coq build.Maxime Dénès
2017-03-23Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-23Merge PR#497: [travis] [8.6.only] Backport latest changes from trunk.Maxime Dénès
2017-03-23Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220."Maxime Dénès
2017-03-23Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-23Merge PR#495: funind: Ignore missing info for current functionMaxime Dénès
2017-03-23Add empty Extraction.v and FunInd.v to prepare landing of PR#220.Maxime Dénès
2017-03-23Merge PR#491: Do not typecheck twice the type of opaque constants.Maxime Dénès
2017-03-23[META] add support for ide librariesEmilio Jesus Gallego Arias
2017-03-22Merge PR#480: show unused intro pattern warningMaxime Dénès
2017-03-22Merge PR#493: [safe-string] update dev/doc/changesMaxime Dénès
2017-03-22Merge PR#415: Use a compact representation for real literalsMaxime Dénès
2017-03-22make check not CoqIDE-specificPaul Steckler
2017-03-22Better compatibility of TACTIC EXTEND AT LEVEL with versions of camlp5.Hugo Herbelin
2017-03-22[travis] Fix iris-coq build.Emilio Jesus Gallego Arias
2017-03-22Document the changes to IZR.Guillaume Melquiond
2017-03-22Make IZR a morphism for field.Guillaume Melquiond
2017-03-22Mark ring morphisms as opaque.Guillaume Melquiond
2017-03-22Change the parser and printer so that they use IZR for real constants.Guillaume Melquiond
2017-03-22[travis] [8.6.only] Backport latest changes from trunk.Emilio Jesus Gallego Arias
2017-03-22Make IZR use a compact representation of integers.Guillaume Melquiond
2017-03-22Fix broken evaluation strategies for ring and field.Guillaume Melquiond
2017-03-22Fix some typos.Guillaume Melquiond
2017-03-22Simplify some proofs using ring and field.Guillaume Melquiond
2017-03-22Remove duplicate lemmas.Guillaume Melquiond
2017-03-22funind: Ignore missing info for current functionTej Chajed
2017-03-22Merge branch 'v8.6'Pierre-Marie Pédrot
2017-03-22Merge PR#390: Updates to the Pretty Printing InfrastructureMaxime Dénès
2017-03-22Merge PR#478: Small optimization on handling of library state.Maxime Dénès
2017-03-22Merge PR#482: [toplevel] Remove unusable option -notopMaxime Dénès
2017-03-21Add a few comments in term_typing.ml.Maxime Dénès
2017-03-21Do not typecheck twice the type of opaque constants.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 09:49:36 +0000