aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-05-31Remove Show Script (deprecated in 8.10)Gaëtan Gilbert
2019-05-31Fix #10268: vio2vo produces incorrect term when discharging.Pierre-Marie Pédrot
2019-05-30Merge PR #10269: Checker: don't use monomorphic universes attached to a constantPierre-Marie Pédrot
2019-05-29Merge PR #10252: Various dynamic assertions and cleanups in opaque typingMaxime Dénès
2019-05-29Merge PR #10248: Move the Discharge module in the kernel and merge it with Co...Maxime Dénès
2019-05-29Merge PR #10270: Fix debug printersEnrico Tassi
2019-05-29Merge PR #10049: [elaboration] Bidirectionality hintsEnrico Tassi
2019-05-29[proofs] Remove unused API [detected by coverage]Emilio Jesus Gallego Arias
2019-05-28Merge PR #10228: gitlab: run less jobs unless FULL_CI=trueEmilio Jesus Gallego Arias
2019-05-28Fix printers.sh test when missing coqtop.byte, print more infoGaëtan Gilbert
2019-05-28Merge PR #10258: Remove the delayed universe table from object files.Enrico Tassi
2019-05-28Fix [Drop. #use "include";;] for indirect_accessorGaëtan Gilbert
2019-05-28[elaboration] Bidirectionality hintsMaxime Dénès
2019-05-28Same universe constraint fix for the checker.Pierre-Marie Pédrot
2019-05-28Checker: don't use monomorphic universes attached to a constantGaëtan Gilbert
2019-05-28Merge PR #10133: mind_kelim is the highest allowed sort instead of a listPierre-Marie Pédrot
2019-05-28Tentative alternative fix for #9992.Pierre-Marie Pédrot
2019-05-28Faster renaming of shadowed variables in evar instance creation.Pierre-Marie Pédrot
2019-05-28Fix #10264: Singleton class field data is erroneous.Pierre-Marie Pédrot
2019-05-27Remove the delayed universe table from object files.Pierre-Marie Pédrot
2019-05-27Merge PR #10249: More precise type for export and inlining of private constantsMaxime Dénès
2019-05-27Fix #10251: Type-checking of polymorphic opaque constr entry types is broken.Pierre-Marie Pédrot
2019-05-27Specific code path for opaque polymorphic constants.Pierre-Marie Pédrot
2019-05-27Ensure dynamically that non-opaque definitions are always side-effect free.Pierre-Marie Pédrot
2019-05-27Ensure dynamically that opaque definitions come with their type.Pierre-Marie Pédrot
2019-05-27gitlab: run less jobs unless FULL_CI=trueGaëtan Gilbert
2019-05-27Overlay for mind_kelim change (#10133)Gaëtan Gilbert
2019-05-27mind_kelim is the highest allowed sort instead of a listGaëtan Gilbert
2019-05-27Merge PR #10241: Update README.md / add SUPPORT.md file.Maxime Dénès
2019-05-27Merge PR #10198: Centralize the hashconsing of constant declarations.Maxime Dénès
2019-05-27Merge PR #10235: [debug] Print restriction metadata in evar map debug printerPierre-Marie Pédrot
2019-05-27Merge PR #10237: Fix some incorrect uses of proof-local environmentPierre-Marie Pédrot
2019-05-27[debug] Print restriction metadata in evar map debug printerMaxime Dénès
2019-05-26Merge PR #10220: Use new coqrst syntax for alternatives in SSReflect chapter.Enrico Tassi
2019-05-26More precise type for Safe_typing export and inlining of private constants.Pierre-Marie Pédrot
2019-05-26Code sharing inside Cooking.Pierre-Marie Pédrot
2019-05-26Actually merge Discharge into Cooking.Pierre-Marie Pédrot
2019-05-26Share API between Discharge and Cooking.Pierre-Marie Pédrot
2019-05-26Move the Discharge module into the kernel.Pierre-Marie Pédrot
2019-05-25Merge PR #10244: Coqc: Treat unknown arguments starting with dash as unknown ...Emilio Jesus Gallego Arias
2019-05-25Merge PR #9288: Giving preference to syntax "injection ... as [= pat1 ... pat...Théo Zimmermann
2019-05-25Coqc: Treat unknown arguments starting with dash as unknown options rather th...Hugo Herbelin
2019-05-25Modifying theories to preferably use the "[= ]" syntax, and,Hugo Herbelin
2019-05-25Documenting syntax "injection ... as [= pat1 ... patn ]".Hugo Herbelin
2019-05-25Centralize the hashconsing of constant declarations.Pierre-Marie Pédrot
2019-05-24Add SUPPORT.md file.Théo Zimmermann
2019-05-24Update README, remove MacPorts link (not updated since 8.8.2).Théo Zimmermann
2019-05-24Merge PR #10233: Fixing typos - Part 3Théo Zimmermann
2019-05-24Use global env in numeral and string notationsMaxime Dénès
2019-05-24Stop using pstate in global print queriesGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 17:47:13 +0000