aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-03-31[ci] Run bignums' testsPierre Roux
2020-03-31Merge PR #11668: Helping issue #11659 by leaving only the Cast hack in the gr...Maxime Dénès
2020-03-31Merge PR #11647: [rfc] Consolidation of parsing interfacesPierre-Marie Pédrot
2020-03-30Merge PR #11725: Cleanup stdlib reals.Hugo Herbelin
2020-03-30Merge PR #11969: ocamlformat: use whitelist instead of blacklistEmilio Jesus Gallego Arias
2020-03-30Merge PR #11965: Partial revert of #11817.Emilio Jesus Gallego Arias
2020-03-30Merge PR #11968: Fix commit hook when there are no changes (eg amend message)Emilio Jesus Gallego Arias
2020-03-30ocamlformat: use whitelist instead of blacklistGaëtan Gilbert
2020-03-30Fix commit hook when there are no changes (eg amend message)Gaëtan Gilbert
2020-03-30Missing apartness notationsVincent Semeria
2020-03-30Partial revert of #11817.Pierre-Marie Pédrot
2020-03-30Merge PR #11921: Remove some cruft from Reductionops API.Gaëtan Gilbert
2020-03-30Merge PR #11817: [cleanup] Remove unnecessary Map/Set module creationGaëtan Gilbert
2020-03-30Merge PR #11951: Remove a useless reversed variant in Vars.Gaëtan Gilbert
2020-03-30Merge PR #11958: Add -no-update command line option to doc_grammar for DuneThéo Zimmermann
2020-03-30Merge PR #11018: “auto with zarith”: use “lia” rather than “omega”Maxime Dénès
2020-03-30Merge PR #11874: Auto-format micromega files in pre-commit hook.Emilio Jesus Gallego Arias
2020-03-29Add -no-update command line option to doc_grammar for DuneJim Fehrle
2020-03-29Merge PR #11938: Support for updating orderedGrammar with Dune.Emilio Jesus Gallego Arias
2020-03-29Merge PR #11859: Warn when non exactly parsing non floating-pointHugo Herbelin
2020-03-29Merge PR #11944: Remove SearchAbout command, deprecated in 8.5Théo Zimmermann
2020-03-28Merge PR #11950: Document change of behavior of Fail in 8.11.Clément Pit-Claudel
2020-03-28Remove a useless reversed variant in Vars.Pierre-Marie Pédrot
2020-03-28Remove some cruft from Reductionops API.Pierre-Marie Pédrot
2020-03-28Remove SearchAbout command, deprecated in 8.5Jim Fehrle
2020-03-28Document change of behavior of Fail in 8.11.Théo Zimmermann
2020-03-28Update fullGrammar and orderedGrammar following #11877.Théo Zimmermann
2020-03-28New target check-gram to check if fullGrammar and orderedGrammar are up-to-date.Théo Zimmermann
2020-03-27Fix changelogVincent Semeria
2020-03-27Merge PR #11809: [configure] Remove `-std=c99` from default C flagsJason Gross
2020-03-27Merge PR #11871: Split documentation of coqdoc on separate page.Clément Pit-Claudel
2020-03-27[configure] Remove `-std=c99` from default C flagsEmilio Jesus Gallego Arias
2020-03-27Cleanup stdlib reals. Use implicit arguments for ConstructiveReals. Move Cons...Vincent Semeria
2020-03-27Helping issue #11659 by leaving only the Cast hack in the grammar.Hugo Herbelin
2020-03-27Merge PR #11848: Nicer printing for decimal constantsHugo Herbelin
2020-03-27Merge PR #11751: Fix #11749: don't warn for hidden files.Maxime Dénès
2020-03-27Merge PR #11102: Use the Alloc_small macro from the OCaml runtime rather than...Maxime Dénès
2020-03-27Split coqdoc section out of utility chapter (octopus merge).Théo Zimmermann
2020-03-27Move section on coqdoc to new location.Théo Zimmermann
2020-03-27Remove the part about coqdoc from the utilities chapter.Théo Zimmermann
2020-03-27Prepare split of section about coqdoc.Théo Zimmermann
2020-03-27Merge PR #11925: [ci] Add bbvEmilio Jesus Gallego Arias
2020-03-26Merge PR #11929: Reintroduce a command that was actually used in another one....Clément Pit-Claudel
2020-03-26Reintroduce commands that were actually used. Fix build of PDF manual.Théo Zimmermann
2020-03-26Merge PR #11877: Removing deprecated destruct/remember syntax _eqn.Théo Zimmermann
2020-03-26Change logHugo Herbelin
2020-03-26Merge PR #11920: Shrink refman-prelude files.Clément Pit-Claudel
2020-03-26[ci] Add bbvJason Gross
2020-03-26CIC is printed in all-caps.Théo Zimmermann
2020-03-26Removing deprecated destruct syntax _eqn.Hugo Herbelin