aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-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-23[ci] add metacoqMatthieu Sozeau
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
2020-03-22Centralizing all kinds of numeral string management in numTok.ml.Hugo Herbelin
2020-03-22Adding bignat to parse positive numbers; bigint now includes negative ints.Hugo Herbelin
2020-03-22Merge PR #11731: [proof] Miscellaneous refactoringsGaëtan Gilbert
2020-03-22Merge PR #11851: Process command line load vernaculars before command line Go...Emilio Jesus Gallego Arias
2020-03-22Merge PR #11855: Build and install refman with Dune.Emilio Jesus Gallego Arias
2020-03-22[proof] Deprecate unused tacmach functions.Emilio Jesus Gallego Arias
2020-03-21Add module ZifyPow to avoid compatibility issue with 8.11.Théo Zimmermann
2020-03-21Reorder the load/require cmd-options and set/unset cmd-optionsLasse Blaauwbroek
2020-03-20Fix the computation of recursive principles with let-bindings.Pierre-Marie Pédrot
2020-03-20Merge PR #11665: Make Cumulative, NonCumulative and Private attributes.Pierre-Marie Pédrot
2020-03-20Merge PR #11814: Document coq_makefile behavior wrt -native-compiler yesEnrico Tassi
2020-03-20Merge PR #11847: Properly thread let-bindings in Funind principle construction.Pierre Courtieu
2020-03-20Merge PR #11778: [ocamformat] Update to 0.13.0Théo Zimmermann
2020-03-20Build and install refman with Dune.Théo Zimmermann
2020-03-20Merge PR #11857: Remove calls to structural equality in MicromegaVincent Laporte
2020-03-19Merge PR #11601: [refman] Move chapters into new structure.Clément Pit-Claudel
2020-03-19[ocamformat] Update to 0.13.0Emilio Jesus Gallego Arias
2020-03-19[obligations] Step towards more structured handling of remaining obligations.Emilio Jesus Gallego Arias
2020-03-19[obligations] Refactor some common code on save pathEmilio Jesus Gallego Arias
2020-03-19[obligations] More progress towards unification of the save pathEmilio Jesus Gallego Arias
2020-03-19[comFixpoint] Cleanup on opens prior to fix unificationEmilio Jesus Gallego Arias
2020-03-19[proof] Remove duplicated poly field in Proof_global.tEmilio Jesus Gallego Arias
2020-03-19[pfedit] Labelize sign parameterEmilio Jesus Gallego Arias
2020-03-19[declare] Remaining bits on the consistency of UState.t namingEmilio Jesus Gallego Arias
2020-03-19[vernac] Make local exception localEmilio Jesus Gallego Arias
2020-03-19[comFixpoing] Refactor hybrid interactive command modalityEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 02:09:29 +0000