aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-05-30Fix #7113: Program Let Fixpoint in section causes anomalyGaëtan Gilbert
2018-05-30overlay triggering bug #7472 (that #7495) is supposed to fixEnrico Tassi
2018-05-30Fix restrict_universe_contextGaëtan Gilbert
2018-05-30Fix an outdated comment refering to lib/dnet.mliArmaël Guéneau
2018-05-29Merge PR #7593: Don't try to install native compiled files if native-compile ...Maxime Dénès
2018-05-29Fix #6951: Unexpected error during scheme creation.Pierre-Marie Pédrot
2018-05-29Merge PR #7566: Remove a dead old-refman file.Maxime Dénès
2018-05-29Merge PR #7628: [default.nix] Update dependency listThéo Zimmermann
2018-05-29Merge PR #7626: Test for #7333 (soundness with VM/native and cofix)Théo Zimmermann
2018-05-29[Makefile] New target “install-merlin”Vincent Laporte
2018-05-29Fix anomaly in autoapply when an unbound hint name is providedArmaël Guéneau
2018-05-29[default.nix] Adds “ounit” to check dependenciesVincent Laporte
2018-05-29[default.nix] List “hostname” as a dependencyVincent Laporte
2018-05-29[default.nix] Use OCaml 4.06Vincent Laporte
2018-05-29[default.nix] Drop dependency to ocp-indexVincent Laporte
2018-05-29Merge PR #7084: [default.nix] Unpin nixpkgsThéo Zimmermann
2018-05-29Add test for #7333: vm_compute segfaults / Anomaly with cofixMaxime Dénès
2018-05-28Merge PR #7521: Fix soundness bug with VM/native and cofixpointsPierre-Marie Pédrot
2018-05-28Tactics.introduction: remove dangerous option ~checkEnrico Tassi
2018-05-28Improve the last section of the Gallina chapter.Théo Zimmermann
2018-05-28Chapter 1 of the refman compiles without reporting any undocumented object.Théo Zimmermann
2018-05-28Improve sections on (Co)Fixpoint of the Gallina chapter.Théo Zimmermann
2018-05-28Add CHANGES entryMaxime Dénès
2018-05-28Fix #7333: vm_compute segfaults / Anomaly with cofixMaxime Dénès
2018-05-28Mention test-suite in PR templateJason Gross
2018-05-28Unify pre_env and envMaxime Dénès
2018-05-28Remove vm_conv hook and reorganize kernel filesMaxime Dénès
2018-05-28Make some comments more precise about compilation of cofixpointsMaxime Dénès
2018-05-28Less confusing debug printing of setfield bytecode instructionMaxime Dénès
2018-05-28Merge PR #7419: Remove 100 occurrences of Evd.emptyPierre-Marie Pédrot
2018-05-27Improve subsection on co-inductive types of the Gallina chapter.Théo Zimmermann
2018-05-27Simplify the code that handles trust of side-effects in kernel typing.Pierre-Marie Pédrot
2018-05-27[api] Make `vernac/` self-contained.Emilio Jesus Gallego Arias
2018-05-27[tactics] Turn boolean locality hint parameter into a named one.Emilio Jesus Gallego Arias
2018-05-27[api] [parsing] Move Egram* to `vernac/`Emilio Jesus Gallego Arias
2018-05-27Improve subsection on mutual inductive types of the Gallina chapter.Théo Zimmermann
2018-05-27Move 'new in Coq 8.1' subsection to an appropriate place.Théo Zimmermann
2018-05-27Document Variant properly.Théo Zimmermann
2018-05-27Improve inductive types subsection of the Gallina chapter.Théo Zimmermann
2018-05-27Merge PR #7573: Remove unused Printer.printer_pr override mechanism.Hugo Herbelin
2018-05-26Merge PR #7543: [ide] Move common protocol library to its own folder/object.Pierre-Marie Pédrot
2018-05-26Improve subsection Definitions of the Gallina chapter.Théo Zimmermann
2018-05-26Improve subsection Assumptions of the Gallina chapter.Théo Zimmermann
2018-05-26Merge PR #7603: Use -j 1 for high memory fiat crypto targetsEmilio Jesus Gallego Arias
2018-05-26Merge PR #7285: Give advice on managing GitHub notifications in CONTRIBUTING.Maxime Dénès
2018-05-26Improve the section Terms of the Gallina chapter.Théo Zimmermann
2018-05-26Merge PR #6057: Start a release process documentation.Maxime Dénès
2018-05-25Allow make clean to work on a fresh cloneJason Gross
2018-05-25[doc] Allow more than one signature and name per Sphinx objectClément Pit-Claudel
2018-05-25Merge pull request #7569 from ppedrot/clean-newringAssia Mahboubi