aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-11-25zify: explicitly use “lia”Vincent Laporte
2019-11-25btauto: use “lia” rather than “omega”Vincent Laporte
2019-11-25PermutEq: use “lia” rather than “omega”Vincent Laporte
2019-11-25PermutSetoid: use “lia” rather than “omega”Vincent Laporte
2019-11-25MSets: use “lia” rather than “omega”Vincent Laporte
2019-11-25Add a complexity test for `pattern`Jason Gross
2019-11-24Merge PR #11152: Cache the relevance flag in rel contexts in an efficient way.Gaëtan Gilbert
2019-11-24fix «W -- weakening» docAntonio Nikishaev
2019-11-22Add test for #11161Gaëtan Gilbert
2019-11-22Merge PR #11136: Adding `inj_compr` lemma in ssrfun.Enrico Tassi
2019-11-22Use the relevance flag in CClosure rel contexts in an efficient way.Pierre-Marie Pédrot
2019-11-21A refined version of #8890 which prevents #11033.Hugo Herbelin
2019-11-21Merge PR #11154: add tlc to ci; please proof read very carefully and test. th...Emilio Jesus Gallego Arias
2019-11-21Merge PR #11145: Document -vos flag for coqdepEmilio Jesus Gallego Arias
2019-11-21Merge PR #11132: Fixing bugs in the computation of implicit arguments for `Fi...Emilio Jesus Gallego Arias
2019-11-21Merge PR #11109: Register proof_irrelevanceEmilio Jesus Gallego Arias
2019-11-21Merge PR #10587: [coqdoc] Nest <a> into <h2> instead of the other way aroundEmilio Jesus Gallego Arias
2019-11-21Merge PR #10614: Update the Gallina grammar in doc, "Terms" sectionThéo Zimmermann
2019-11-21Merge PR #11010: [coq] Untabify the whole ML codebase.Gaëtan Gilbert
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-21add tlc to ci; please proof read very carefully and test. thankscharguer
2019-11-21Document -vos flag for coqdepGaëtan Gilbert
2019-11-21Update doc/changelog/02-specification-language/11132-master+fix-implicit-let-...Hugo Herbelin
2019-11-21Merge PR #11103: Grammars: unification fix/cofix between constr/vernac + clea...Emilio Jesus Gallego Arias
2019-11-21Merge PR #11075: load .vo when .vos is missing + misc vos changesEmilio Jesus Gallego Arias
2019-11-21Taking @Zimmi48's comment into accountCyril Cohen
2019-11-20Merge PR #11144: Fix broken linksThéo Zimmermann
2019-11-20Fix broken linksNikita Eshkeev
2019-11-20Update grammar in the Terms section of Gallina chapterJim Fehrle
2019-11-20Merge PR #11119: 8.10-backportable part of #10575Clément Pit-Claudel
2019-11-20Combine similar arguments when printing Arguments commandGaëtan Gilbert
2019-11-20make VernacArguments closer to user syntaxGaëtan Gilbert
2019-11-20From CoqIDE or -vos or -vok compilation, load .vo when .vos is missing (fixin...charguer
2019-11-20Merge PR #11068: coq_makefile: support COQBIN with no ending /Enrico Tassi
2019-11-20Merge PR #11074: coqdep: only output vos when passed -vosEmilio Jesus Gallego Arias
2019-11-19G_constr: Renaming record_fields_instance -> fields_def.Hugo Herbelin
2019-11-19G_constr: Renaming instance -> univ_instance (more specific name).Hugo Herbelin
2019-11-19G_constr: Uniformization of indentation.Hugo Herbelin
2019-11-19Separating constr grammar for fix and cofix, for the purpose of documentation.Hugo Herbelin
2019-11-19Grammar: slight simplification of treatment of annot/binder overlapping.Hugo Herbelin
2019-11-19Grammar: mini-factorization between fix/cofix and Fixpoint/CoFixpoint.Hugo Herbelin
2019-11-19Grammar of terms: mini-shortcut in the rules for fix and cofix.Hugo Herbelin
2019-11-19Fixing bugs in the computation of implicit arguments for fix with a let binder.Hugo Herbelin
2019-11-19coq_makefile: support COQBIN with no ending /Gaëtan Gilbert
2019-11-19Merge PR #11106: Printing name of change log file in changelog scriptGaëtan Gilbert
2019-11-19added changelog entryCyril Cohen
2019-11-18Adding `inj_compr` lemma in ssrfun.Cyril Cohen
2019-11-18Merge PR #11115: [dune] Update .gitignore after #11092Emilio Jesus Gallego Arias
2019-11-16Merge PR #10996: Refine Instance returnsPierre-Marie Pédrot
2019-11-16Merge PR #10998: Add missing zify class instancesFrédéric Besson