aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-26Fix calling test suite makefile with a dune built coqGaëtan Gilbert
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
2020-03-26Shrink refman-prelude files.Théo Zimmermann
2020-03-26Merge PR #11918: Fix #11845: anomaly when including partially applied functorPierre-Marie Pédrot
2020-03-26Merge PR #11919: Remove outdated mention of -allow-sprop.Gaëtan Gilbert
2020-03-26Remove outdated mention of -allow-sprop.Théo Zimmermann
2020-03-26Fix #11845: anomaly when including partially applied functorGaëtan Gilbert
2020-03-26Merge PR #11913: Doc_grammar: Update cmd:: and tacn:: constructs in .rstsThéo Zimmermann
2020-03-26Merge PR #11832: [ocamlformat] Use doc-comments=before style.Théo Zimmermann
2020-03-26Merge PR #11885: Sorting: Swap the names of Sorted_sort and LocallySorted_sortHugo Herbelin
2020-03-26Merge PR #11891: Fix levels of `<=?` and `<?` in the stdlibHugo Herbelin
2020-03-26Print a warning when parsing non floating-point values.Pierre Roux
2020-03-25[gramlib] Don't expose unsafe interfaces to clientsEmilio Jesus Gallego Arias
2020-03-25[pcoq] Inline the exported Gramlib interface instead of exposing it as GEmilio Jesus Gallego Arias
2020-03-25[parsing] Move comments lexer extensions to base lexer interfaceEmilio Jesus Gallego Arias
2020-03-25[gramlib] Remove warning function parameter in favor of standard mechanism.Emilio Jesus Gallego Arias
2020-03-25[parsing] Move `coq_parsable` custom logic to Grammar.Emilio Jesus Gallego Arias
2020-03-25[parsing] Remove redundant interfaces from PcoqEmilio Jesus Gallego Arias
2020-03-25[parsing] Remove unneeded `Extend.entry` type.Emilio Jesus Gallego Arias
2020-03-25[parsing] Remove extend AST in favor of gramlib constructorsEmilio Jesus Gallego Arias
2020-03-25[parsing] Make grammar rules private.Emilio Jesus Gallego Arias
2020-03-25[parsing] Make grammar extension type private.Emilio Jesus Gallego Arias
2020-03-25[gitlab] Increase flambda stack size.Emilio Jesus Gallego Arias
2020-03-25Merge PR #11898: Switch opam file to makeEmilio Jesus Gallego Arias
2020-03-25[ocamlformat] Use doc-comments=before style.Emilio Jesus Gallego Arias
2020-03-25Doc_grammar: Update cmd:: and tacn:: constructs in .rstsJim Fehrle
2020-03-25Merge PR #11705: Convert Gallina Extensions chapter to use prodnsThéo Zimmermann
2020-03-25Convert Gallina Extensions to use prodnJim Fehrle
2020-03-25Make the level of ≡ in Int63 consistent with =Jason Gross