aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-02-20Adding changelog.Hugo Herbelin
2020-02-20Fixing #11114 (anomaly with Extraction Implicit on records).Hugo Herbelin
2020-02-19Merge PR #11499: Clarify expectations for overlay creationEmilio Jesus Gallego Arias
2020-02-19Merge PR #11302: Add --fuzz, --real, --user to timing scriptsEmilio Jesus Gallego Arias
2020-02-19Merge PR #11636: Revert buggy commit mistakenly pushed with #11530Emilio Jesus Gallego Arias
2020-02-19Merge PR #11600: New syntax [Inductive Acc A R | x : Prop := ...]Emilio Jesus Gallego Arias
2020-02-19Revert "Granting #9516 and #9518 (support for numerals and strings in custom ...Hugo Herbelin
2020-02-18Merge PR #11530: Fixes custom entries precedence bugs (#11331 part)Pierre-Marie Pédrot
2020-02-18Merge PR #11529: [build] Consolidate stdlib's .v files under a single directory.Théo Zimmermann
2020-02-18Merge PR #10204: Remove `unsafe_type_of` from `Coercion`Gaëtan Gilbert
2020-02-17Merge PR #11350: stdlib List: add [remove'] and [count_occ'] that use [filter]Hugo Herbelin
2020-02-17Merge PR #11593: Update bug report address in coqwc man page.Théo Zimmermann
2020-02-17Merge PR #11614: Show apostrophes and backticks in HTML doc, too.Théo Zimmermann
2020-02-17Merge PR #11589: [coqdep] Remove support for `-c` ocamldep replacement.Gaëtan Gilbert
2020-02-17New syntax [Inductive Acc A R | x : Prop := ...]Gaëtan Gilbert
2020-02-17Revert "Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)"Gaëtan Gilbert
2020-02-16Show apostrophes and backticks in HTML, too.Jim Fehrle
2020-02-16Revert "Suite picking numeral notation"Hugo Herbelin
2020-02-16Suite picking numeral notationHugo Herbelin
2020-02-16Granting #9516 and #9518 (support for numerals and strings in custom entries).Hugo Herbelin
2020-02-16Adding change log.Hugo Herbelin
2020-02-16Fixing bug #9521 (anomaly due to missing declaration of level in custom entry).Hugo Herbelin
2020-02-16Mini-factorization in vernac grammar.Hugo Herbelin
2020-02-16Custom entries: accept that no level is mentioned for a subentry.Hugo Herbelin
2020-02-15Reusing type production_level for the result of adjust_level.Hugo Herbelin
2020-02-15Reorganize type "production_level" along a more intuitive structure.Hugo Herbelin
2020-02-15Dead code in Egramcoq.adjust_level.Hugo Herbelin
2020-02-15Fixing a precedence printing bug with custom entries.Hugo Herbelin
2020-02-15Fixes #11331 (unexpected level collisions between custom entries and constr).Hugo Herbelin
2020-02-14Merge pull request #11605 from ppedrot/ltac2-annotate-match-branchKenji Maillard
2020-02-14Merge PR #11557: Use thunks to univ instead of lazy constr for template typingPierre-Marie Pédrot
2020-02-14Apply suggestions from code reviewJason Gross
2020-02-14Annotate Ltac2 match macro variables with their type.Pierre-Marie Pédrot
2020-02-14Merge PR #11599: Spell out index entry suffixes in main index, e.g. "(tactic)...Théo Zimmermann
2020-02-14Merge PR #11468: [doc] fix typo & update release-process.md for opam/docker p...Théo Zimmermann
2020-02-14Overlay for Inductive.type_of_inductive doesn't take an envGaëtan Gilbert
2020-02-14Use thunks to univ instead of lazy constr for template typingGaëtan Gilbert
2020-02-14Merge PR #11584: Add #[uniform] and #[nonuniform] (for Uniform Inductive Para...Maxime Dénès
2020-02-13Spell out the entry suffix in the main indexJim Fehrle
2020-02-13[coqdep] Remove support for `-c` ocamldep replacement.Emilio Jesus Gallego Arias
2020-02-13[coqdep] Merge `-sort` and `-suffix` options.Emilio Jesus Gallego Arias
2020-02-13Merge PR #11427: Dispatch code ownership of files in dev/doc.Emilio Jesus Gallego Arias
2020-02-13Merge PR #11450: Publishing a new version on Zenodo: not a relevant step for ...Emilio Jesus Gallego Arias
2020-02-13Merge PR #11441: Add explicit types to changelog entries that were still miss...Emilio Jesus Gallego Arias
2020-02-13[coqinit] Removed unused `with_ml` parameter.Emilio Jesus Gallego Arias
2020-02-13[build] Consolidate stdlib's .v files under a single directory.Emilio Jesus Gallego Arias
2020-02-13Merge PR #11564: Recognize Default Proof Using in STMEnrico Tassi
2020-02-13Merge PR #11417: Move kind_of_type from the kernel to EConstr.Enrico Tassi
2020-02-13Merge PR #11098: Let Arguments support anonymous implicit argumentsEmilio Jesus Gallego Arias
2020-02-13Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-23 14:43:27 +0000