aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-11Update doc/sphinx/practical-tools/utilities.rstJason Gross
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-11Add paramcoq overlayMaxime Dénès
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
2020-02-09Remove the Template Check option.Pierre-Marie Pédrot
2020-02-09Merge PR #11551: Remove -compat 8.9.Emilio Jesus Gallego Arias
2020-02-09Merge PR #11550: Fixing wrong comments in context.mlPierre-Marie Pédrot
2020-02-09Fix #11553: magicaly_constant_of_fixbody checks existence of made up constantGaëtan Gilbert
2020-02-08Remove -compat 8.9.Théo Zimmermann
2020-02-08Merge PR #11240: Add rew dependent NotationsHugo Herbelin
2020-02-08Merge PR #10343: Resolve 10342 : [Ltac2] Add array libraryPierre-Marie Pédrot
2020-02-08Merge PR #11404: replace RList by list R in all files where it is used in thi...Pierre-Marie Pédrot
2020-02-08Fixing wrong comments in context.ml.Hugo Herbelin
2020-02-08Resolve #10342 : [Ltac2] Add array libraryMichael Soegtrop
2020-02-07Merge PR #11523: [coqdep] Several refactoring and consolidationsGaëtan Gilbert
2020-02-07Remove unsafe_type_of from funindGaëtan Gilbert
2020-02-07various unsafe_type_of -> type_of_variable in funindGaëtan Gilbert
2020-02-07Remove confusing commented code in funindGaëtan Gilbert
2020-02-07Merge PR #11528: Checker does not rely on Monomorphic fieldsGaëtan Gilbert
2020-02-07[coqdep] Add changelog for recent modifications.Emilio Jesus Gallego Arias
2020-02-07[coqdep] Don't treat stdlib specially in boot mode.Emilio Jesus Gallego Arias
2020-02-07[coqdep] Remove deprecated -slash , unused, undocumented -mldep option.Emilio Jesus Gallego Arias
2020-02-07[coqdep] Remove dumpgraph and broken optionsEmilio Jesus Gallego Arias
2020-02-07Merge PR #11543: restore the default URL for coquelicotThéo Zimmermann
2020-02-07restore the default URL for coquelicotYves Bertot
2020-02-06Apply suggestions from code reviewJason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-13 20:26:45 +0000