aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-02-14Merge PR #11584: Add #[uniform] and #[nonuniform] (for Uniform Inductive Para...Maxime Dénès
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-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
2020-02-13Delete unused commentGaëtan Gilbert
2020-02-13Don't duplicate the inductive keyword for each block elt when parsingGaëtan Gilbert
2020-02-13Merge PR #11407: [mltop] Store digest of modules used to compile files.Gaëtan Gilbert
2020-02-13Merge PR #11521: Remove Goptions.opt_name fieldPierre-Marie Pédrot
2020-02-13Merge PR #11457: [toplevel] Refactor control loopHugo Herbelin
2020-02-13Merge PR #11424: Check instance length in type_of_{inductive,constructor}Pierre-Marie Pédrot
2020-02-13Merge PR #11577: [nix] Fix building of the documentationThéo Zimmermann
2020-02-13Arguments: removing the restriction to set an anonymous parameter implicit.Hugo Herbelin
2020-02-13Implicit arguments: Fixing count of the position in compute_implicit_statuses.Hugo Herbelin
2020-02-12Merge PR #11582: Split unicoq out of ci-mtac2.sh (keeping 1 CI job)Emilio Jesus Gallego Arias
2020-02-12Split unicoq out of ci-mtac2.sh (keeping 1 CI job)Gaëtan Gilbert
2020-02-12[toplevel] Make toplevel loop tail-recursive againEmilio Jesus Gallego Arias
2020-02-12[toplevel] Refactor control loopEmilio Jesus Gallego Arias
2020-02-12Merge PR #11544: Cleanup some globref related manipulationsPierre-Marie Pédrot
2020-02-12overlay for removal of optnameGaëtan Gilbert
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2020-02-12Merge PR #11569: Remove unused Environ.push_constraints_to_envPierre-Marie Pédrot
2020-02-12Merge PR #11563: Mini improvement of the formatting rule for printing fix and...Gaëtan Gilbert
2020-02-12Check instance length in type_of_{inductive,constructor}Gaëtan Gilbert
2020-02-12Standardize constr -> globref operations to use destRef/isRef/isRefXGaëtan Gilbert
2020-02-12ReferenceVariables error contains a globref instead of a constrGaëtan Gilbert
2020-02-12Merge PR #11556: [coqdep] mli cleanup, remove unused functionsGaëtan Gilbert
2020-02-12Merge PR #11546: Remove the Template Check option.Gaëtan Gilbert
2020-02-12[nix] Fix building of the documentationVincent Laporte
2020-02-12Merge PR #11573: Fixing extra space in front of keywords in Print GrammarEmilio Jesus Gallego Arias
2020-02-11Merge PR #11509: Add changelog and fixes for #10202Emilio Jesus Gallego Arias
2020-02-11Fixing extra space in "Print Grammar" (i.e. Grammar.Entry.print in Gramlib).Hugo Herbelin
2020-02-11Merge PR #11494: Remove fiat-crypto-legacy from CIGaëtan Gilbert
2020-02-11Remove fiat-crypto-legacy from CIMaxime Dénès
2020-02-11Document the ability to use manual implicit arguments in subexpressions.Hugo Herbelin
2020-02-11Fixing some residual bugs of PR #10202 (manual implicit args in subterms).Hugo Herbelin
2020-02-11Reinforcing the role of type "typing_constraint".Hugo Herbelin
2020-02-11Lately adding a changelog for PR#10202.Hugo Herbelin
2020-02-11Remove unused Environ.push_constraints_to_envGaëtan Gilbert
2020-02-11Merge PR #11235: Add syntax for non maximal implicit argumentsHugo Herbelin
2020-02-11Another micro-improvement in printing "fix".Hugo Herbelin
2020-02-11Small improvement to "fix"/"cofix" printing rule.Hugo Herbelin
2020-02-11[coqdep] mli cleanup, remove unused functionsEmilio Jesus Gallego Arias
2020-02-11Merge PR #11554: Fix #11553: magicaly_constant_of_fixbody checks existence of...Pierre-Marie Pédrot
2020-02-11Merge PR #11538: Remove many unsafe_type_of usesPierre-Marie Pédrot
2020-02-10Recognize Default Proof Using in STMTej Chajed
2020-02-09Merge PR #11518: Fix #11515: Ltac2 rewrite on wildcard.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 01:42:35 +0000