aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-03-26CIC is printed in all-caps.Théo Zimmermann
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-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-25Merge PR #11785: [proof] consolidation of mutual definition declaration pathGaëtan Gilbert
2020-03-25Merge PR #11875: Fix deploy of refman following #11855.Gaëtan Gilbert
2020-03-25Add a specific opam file to build te docker imagePierre Roux
2020-03-25[declare] make restrict_ucontext an optional parameter.Emilio Jesus Gallego Arias
2020-03-25[lemmas] Use direct-style for mutual lemma declaration.Emilio Jesus Gallego Arias
2020-03-25[lemmas] Use direct-style for variable declaration.Emilio Jesus Gallego Arias
2020-03-25[proof] [mutual] Factorize mutual per-entry informationEmilio Jesus Gallego Arias
2020-03-25[proof] [mutual] Factorize universe handling.Emilio Jesus Gallego Arias
2020-03-25[proof] [mutual] Factorize mutual body construction.Emilio Jesus Gallego Arias
2020-03-25[proof] [mutual] Factorize notation declaration.Emilio Jesus Gallego Arias
2020-03-25[proof] Factorize call info message in mutual declarationsEmilio Jesus Gallego Arias
2020-03-25[proof] Start of mutual definition save refactoring.Emilio Jesus Gallego Arias
2020-03-24Merge PR #11703: Making of NumTok an API for numeralPierre-Marie Pédrot
2020-03-24Merge PR #11772: [obligations] Don't allocate libobjects for obligation info.Pierre-Marie Pédrot
2020-03-24Merge PR #11826: [proof] Deprecate unused tacmach functions.Pierre-Marie Pédrot
2020-03-24Merge PR #11858: Rename Retypeops -> RelevanceopsPierre-Marie Pédrot
2020-03-24Fix world and watch targets of Makefile.dune now that doc has install rules.Théo Zimmermann
2020-03-24Fix deploy of refman following #11855.Théo Zimmermann
2020-03-24Merge PR #11892: [refman] Fix caching, which was broken by the addition of co...Théo Zimmermann
2020-03-23Merge PR #9607: [ci] add metacoqGaëtan Gilbert
2020-03-23[refman] Fix caching, which was broken by the addition of coq_configClément Pit-Claudel
2020-03-23Fix levels of `<=?` and `<?` in the stdlibJason Gross
2020-03-23[ci] add metacoqMatthieu Sozeau
2020-03-23Sorting: Swap the names of Sorted_sort and LocallySorted_sortLysxia
2020-03-23Merge PR #11888: Fix broken links in prodn:: in docThéo Zimmermann
2020-03-23Merge PR #11867: Fix the computation of recursive principles with let-bindings.Enrico Tassi
2020-03-23Merge PR #11442: Add module ZifyPow to avoid compatibility issue with 8.11.Frédéric Besson
2020-03-22Format hyperlink targets and link ids with the same nameJim Fehrle
2020-03-22[obligations] Don't allocate libobjects for obligation info.Emilio Jesus Gallego Arias
2020-03-22[obligations] Small cleanup for openEmilio Jesus Gallego Arias
2020-03-22Testing notations which are specific numerals.Hugo Herbelin
2020-03-22Adding support for parsing "+" sig in NumTok.Hugo Herbelin
2020-03-22Overlay for QuickChickHugo Herbelin
2020-03-22Adding a test for printing single characters.Hugo Herbelin
2020-03-22Test-suite: Assume coqtop output is text even with non-printable characters.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 19:37:06 +0000