aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-01-25[Numeral notations] Lazy resolution of decimal typesVincent Laporte
2019-01-25[Numeral notations] Use Coqlib registered constantsVincent Laporte
2019-01-24Merge PR #9325: Stop [Print] from saying [is (not) universe polymorphic].Hugo Herbelin
2019-01-24Merge PR #9384: Improve the note in the beginning of the Ltac chapter.Clément Pit-Claudel
2019-01-24Merge PR #9269: Move and rewrite intro pattern sectionThéo Zimmermann
2019-01-24Merge PR #9392: Fix small errors in cic.rst.Théo Zimmermann
2019-01-24Merge PR #9394: [nix-ci] MaintenanceThéo Zimmermann
2019-01-24[nix-CI] Split the build inputsVincent Laporte
2019-01-24[Nix-ci] Add QuickChickVincent Laporte
2019-01-24[Nix-ci] Fix UnicoqVincent Laporte
2019-01-24[Nix-ci] Add formal-topologyVincent Laporte
2019-01-24Merge PR #9377: [CS] recognize applied primitive projections as keys (fix #9375)Matthieu Sozeau
2019-01-24Merge PR #9372: [thread] protect threads against sigalrmEmilio Jesus Gallego Arias
2019-01-24add commentEnrico Tassi
2019-01-24use \nO, \nS, etc. fix \kw{n}.Tanaka Akira
2019-01-24Fix small errors in cic.rst.Tanaka Akira
2019-01-23Move and rewrite documentation for intro patterns that was underJim Fehrle
2019-01-23Merge PR #9357: Fix recursive loadpath of ML filesEmilio Jesus Gallego Arias
2019-01-23Merge PR #9043: [windows] Cleanup cruft from `dev/build/windows`Michael Soegtrop
2019-01-23Merge PR #9270: Turn `Refine instance Mode` off by defaultPierre-Marie Pédrot
2019-01-23Merge PR #9374: Documentation: ring and field simplify can take no argumentsThéo Zimmermann
2019-01-23Fix the information of the level of ; vs ; [ ]Théo Zimmermann
2019-01-23Merge PR #9347: At Qed, if shelved goals remain, emit a warning instead of an...Pierre-Marie Pédrot
2019-01-23Merge PR #9337: Fixing #9329: registering empty levels in the order they are ...Emilio Jesus Gallego Arias
2019-01-23Merge PR #9339: Move plugin tutorial to team ownershipEmilio Jesus Gallego Arias
2019-01-23Improve the note in the beginning of the Ltac chapter.Théo Zimmermann
2019-01-23Merge PR #9361: Make prvect tail recursive (fix #9355)Emilio Jesus Gallego Arias
2019-01-23Merge PR #9382: Transfer maintenance of appveyor infrastructure to the CI teamThéo Zimmermann
2019-01-23Merge PR #9239: [ci] [appveyor] Pass -j2 to Appveyor's build and build test s...Maxime Dénès
2019-01-22Remove unneeded | in productionlistsJim Fehrle
2019-01-22Transfer maintenance of appveyor infrastructure to the CI teamMaxime Dénès
2019-01-22Merge PR #9225: Fix issue: Windows CI: cygwin install cache is not reused #9212Maxime Dénès
2019-01-22[configure] print Sys.os_type since Architecture alone is ambigousEnrico Tassi
2019-01-22[thread] protect threads against sigalrmEnrico Tassi
2019-01-22Fixing #9329 (registering empty levels in the order they are recomputed).Hugo Herbelin
2019-01-22Merge PR #9308: Remove outdated gitignore coqprojectfile.mlEmilio Jesus Gallego Arias
2019-01-22Merge PR #9332: Add OSX job to azureEmilio Jesus Gallego Arias
2019-01-22Make prvect tail recursive (fix #9355)Gaëtan Gilbert
2019-01-22Turn `Refine Instance Mode` off by defaultMaxime Dénès
2019-01-22Make `Add Morphism` not rely on Refine InstanceMaxime Dénès
2019-01-22Remove useless freshness check in new_instanceMaxime Dénès
2019-01-22Distinguish ASTs for Instance and Declare InstanceMaxime Dénès
2019-01-22Simplify parsing of instance bindersMaxime Dénès
2019-01-22VernacDeclareClass -> VernacExistingClassMaxime Dénès
2019-01-22VernacDeclareInstances -> VernacExistingInstanceMaxime Dénès
2019-01-22[CS] recognize applied primitive projections as keys (fix #9375)Enrico Tassi
2019-01-21ring and field simplify can take no argumentsthery
2019-01-21Merge PR #9027: Refactor checking of inductive typesMaxime Dénès
2019-01-21Move plugin tutorial to team ownershipGaëtan Gilbert
2019-01-21Add OSX job to azureGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 14:21:04 +0000