aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-03-30Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-30Merge PR#463: Run non-tactic comands without resilient_commandMaxime Dénès
2017-03-30Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R.Guillaume Melquiond
2017-03-30Merge PR#469: Added take to VectorDefMaxime Dénès
2017-03-30Added take to VectorDef.George Stelle
2017-03-30Merge PR#511: [stm] Remove some obsolete vernacs/classification.Maxime Dénès
2017-03-29Merge PR#522: [coqide] Protect against size_allocate race in proofview.Maxime Dénès
2017-03-29Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-29Merge PR#514: [travis] Backport from trunk: VSTMaxime Dénès
2017-03-29Merge PR#506: [nit] Fix a couple incorrect uses of msg_error.Maxime Dénès
2017-03-29Merge PR#521: Do so that "About" tells if a reference is a coercion.Maxime Dénès
2017-03-29Merge PR#525: [ide] Fix typo in pp serialization.Maxime Dénès
2017-03-29Run non-tactic comands without resilient_commandTej Chajed
2017-03-29[ide] Fix typo in pp serialization.Emilio Jesus Gallego Arias
2017-03-28Fixing missing PropFacts.v in Logic/vo.itarget.Hugo Herbelin
2017-03-28[coqide] Protect against size_allocate race in proofview.Emilio Jesus Gallego Arias
2017-03-27Do so that "About" tells if a reference is a coercion.Hugo Herbelin
2017-03-24[travis] Backport from trunk: VSTEmilio Jesus Gallego Arias
2017-03-24Merge PR#489: [travis] Add VSTMaxime Dénès
2017-03-24[stm] Remove some obsolete vernacs/classification.Emilio Jesus Gallego Arias
2017-03-24[nit] Fix a couple incorrect uses of msg_error.Emilio Jesus Gallego Arias
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-08 09:16:27 +0000