aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-09-03Add lemmas directly relating List.nth and List.nth_errorOliver Nash
2019-09-03Remove redundant parameter in List.concat_filter_mapOliver Nash
2019-09-03Add missing index for From ... Require ...Théo Zimmermann
2019-09-03Locations for notation deprecation warningsMaxime Dénès
2019-09-03Merge PR #10651: New lemmas for List.vHugo Herbelin
2019-09-03Apply suggestions from code reviewOliver Nash
2019-09-03New lemmas for List.vOliver Nash
2019-09-02Merge PR #10645: [ci] Update to OCaml 4.08.1Gaëtan Gilbert
2019-09-02Merge PR #10719: Make SSR congr tactic work on arrows in Type.Enrico Tassi
2019-09-02Merge PR #10648: [extraction] Fix #7191: Avoid unsound eta-reductionMaxime Dénès
2019-09-02Merge PR #10562: [library] Move library to vernacMaxime Dénès
2019-09-02Merge PR #10716: [funind] Don't export duplicate save function.Pierre-Marie Pédrot
2019-09-02Merge PR #9918: Fix #9294: critical bug with template polymorphismPierre-Marie Pédrot
2019-09-01edits per reviewYishuai Li
2019-09-01Changelog: more accurate on unconsYishuai Li
2019-09-01Vectors: lemmas about uncons and splitAtYishuai Li
2019-08-30[library] Move library to vernacEmilio Jesus Gallego Arias
2019-08-30Adding a critical-bugs entry. Description from Hugo Herbelin.Pierre-Marie Pédrot
2019-08-30Merge PR #10714: Solve universe error with SSR 'rewrite !term'Pierre-Marie Pédrot
2019-08-30Make SSR congr tactic work on arrows in Type.Andreas Lynge
2019-08-29Solve universe error with SSR 'rewrite !term'Andreas Lynge
2019-08-29Merge PR #10693: Create a maintainer team for the contributing process files.Maxime Dénès
2019-08-29[funind] Don't export duplicate save function.Emilio Jesus Gallego Arias
2019-08-29Merge PR #10674: [declare] Move proof_entry type to declare, put interactive ...Pierre-Marie Pédrot
2019-08-29Merge PR #10660: [cleanup] Replace uses of UserError constructor, clarify exc...Pierre-Marie Pédrot
2019-08-29Merge PR #9066: [parsing] Move pcoq-specific parts in extend to pcoq.Pierre-Marie Pédrot
2019-08-29Merge PR #10703: Make Bool.eqb_spec transparentHugo Herbelin
2019-08-29Merge PR #10643: [glob/aux files] Remove undocumented Stdout dump, cleanup fl...Hugo Herbelin
2019-08-29Fix a few wrong uses of `msg_notice`Maxime Dénès
2019-08-29Make sure that all query commands return a notice (not an info) feedbackMaxime Dénès
2019-08-29Remove wrong advice to base feedback level choice on encoding issuesMaxime Dénès
2019-08-29Logic monad debug printer now emits a debug messageMaxime Dénès
2019-08-28Merge PR #10488: Simplify picking between uint63_63.ml and uint63_31.ml + mak...Enrico Tassi
2019-08-28Merge PR #10646: Recommend assigning an issue before fixing a bug.Emilio Jesus Gallego Arias
2019-08-28Merge PR #10709: Add missing entry to the contributing guide TOC.Emilio Jesus Gallego Arias
2019-08-27[ci] Update to OCaml 4.08.1Emilio Jesus Gallego Arias
2019-08-27[declare] Use entry constructor instead of low-level record.Emilio Jesus Gallego Arias
2019-08-27Merge PR #10680: Tauto: use Coqlib to locate “not” and “NNPP”Pierre-Marie Pédrot
2019-08-27[declare] Move proof_entry type to declare, put interactive proof data on top...Emilio Jesus Gallego Arias
2019-08-27[cleanup] Replace uses of UserError constructor, clarify exception names.Emilio Jesus Gallego Arias
2019-08-27Merge PR #10635: [funind] Port indfun to the new tactic engine.Pierre-Marie Pédrot
2019-08-27Add missing entry to the contributing guide TOC.Théo Zimmermann
2019-08-26Test-suite fixes from HugoMatthieu Sozeau
2019-08-26Document `Template Check` flag and add changelog entry for 9918Matthieu Sozeau
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-08-26Tauto: use Coqlib to locate “not” and “NNPP”Vincent Laporte
2019-08-26Merge PR #10677: coqchk: Cleanup environment manipulation in check_constant_d...Pierre-Marie Pédrot
2019-08-26Merge PR #10696: [lib] [future] Small cleanup of ununsed functions.Pierre-Marie Pédrot
2019-08-26[glob/aux files] Remove undocumented Stdout dump, cleanup flags.Emilio Jesus Gallego Arias
2019-08-26[lib] [future] Small cleanup of ununsed functions.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 22:09:43 +0000