aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-10-30Merge PR #10981: [abstract] Remove un-unused reference to `evar_map`Pierre-Marie Pédrot
2019-10-30Merge PR #10303: Raise an anomaly when looking up unknown constant/inductivePierre-Marie Pédrot
2019-10-30Merge PR #10949: [declare] Provide helper for private constant inlining.Pierre-Marie Pédrot
2019-10-30Merge PR #10681: [declare] Make `proof_entry` a private type.Pierre-Marie Pédrot
2019-10-30Merge PR #10494: Show diffs in "Show Proof."Enrico Tassi
2019-10-29Merge PR #10966: `assert_succeeds`&`assert_fails`: multisuccess fixGaëtan Gilbert
2019-10-29Show diffs in "Show Proof."Jim Fehrle
2019-10-29Use a less kludgy way of solving #9114Jason Gross
2019-10-29Fix #9114, assert_succeeds (exact I) solves goalJason Gross
2019-10-29`assert_succeeds`&`assert_fails`: multisuccess fixJason Gross
2019-10-29[abstract] Remove un-unused reference to `evar_map`Emilio Jesus Gallego Arias
2019-10-29[declare] Use helper function for `fix_exn` instead of relying on internals.Emilio Jesus Gallego Arias
2019-10-29[declare] Make `proof_entry` a private type.Emilio Jesus Gallego Arias
2019-10-29Merge PR #10892: [engine] Remove UnivGen.global_of_constrPierre-Marie Pédrot
2019-10-29Merge PR #10942: Describe XML tags used for highlighting diff textThéo Zimmermann
2019-10-29Merge PR #10947: Rename `VDFILE` from `.coqdeps.d` to `.<CoqMakefile>.d` in `...Enrico Tassi
2019-10-28Merge PR #10963: Possible simplification of parsing rules.Clément Pit-Claudel
2019-10-28Rename `VDFILE` from `.coqdeps.d` to `.<CoqMakefile>.d` in the `coq_makefile`...Kazuhiko Sakaguchi
2019-10-28[declare] Provide helper for private constant inlining.Emilio Jesus Gallego Arias
2019-10-28Fix typos.Théo Zimmermann
2019-10-28Merge PR #10944: [meta] Add zify plugin to META file.Vincent Laporte
2019-10-28Merge PR #10950: [declare] Split universe and inductive declaration code to v...Gaëtan Gilbert
2019-10-28Merge PR #10952: [library] [nit] Remove unnecessary type alias.Gaëtan Gilbert
2019-10-28Add changelog for #10963.Théo Zimmermann
2019-10-28Merge PR #10976: Fix link to `coq-notes.md`Théo Zimmermann
2019-10-27Merge PR #10827: Replace classical reals quotient axioms by functional extens...Hugo Herbelin
2019-10-27Fix link to `coq-notes.md`Michael D. Adams
2019-10-26Merge PR #10516: [funind] Remove duplicate save function.Gaëtan Gilbert
2019-10-25Merge PR #10962: Add missing instances for `implb` and `xorb` in ZifyBool.vFrédéric Besson
2019-10-25Add 2 missing instances in ZifyBool.vKazuhiko Sakaguchi
2019-10-25Possible simplification of parsing rules.Théo Zimmermann
2019-10-25[funind] Remove duplicate save function.Emilio Jesus Gallego Arias
2019-10-25[declare] Generalize kind type on declareDefEmilio Jesus Gallego Arias
2019-10-25[funind] Removed dead code.Emilio Jesus Gallego Arias
2019-10-25[vernac] [inductive] Remove unused internal export.Emilio Jesus Gallego Arias
2019-10-25[inductive] [declare] Move full inductive declaration to declareIndEmilio Jesus Gallego Arias
2019-10-24Merge PR #10943: [meta] Add plugin stanza to META so Fl_dynload works for Coq...Vincent Laporte
2019-10-24Replace classical reals quotient axioms by functional extensionality. Define ...Vincent Semeria
2019-10-24[declare] Split inductive declaration code to vernac/Emilio Jesus Gallego Arias
2019-10-24[declare] Split universe declaration code to vernac/Emilio Jesus Gallego Arias
2019-10-24[library] [nit] Remove unnecessary type alias.Emilio Jesus Gallego Arias
2019-10-24Describe XML tags used for highlighting diff textJim Fehrle
2019-10-24[meta] Add plugin stanza to META so Fl_dynload works for Coq pluginsEmilio Jesus Gallego Arias
2019-10-24Raise an anomaly when looking up unknown constant/inductiveGaëtan Gilbert
2019-10-24Merge PR #10945: Release notes for Coq 8.10.1Théo Zimmermann
2019-10-24Release notes for Coq 8.10.1Vincent Laporte
2019-10-24Merge PR #10938: Better wording for "Show Proof" and fix typosThéo Zimmermann
2019-10-24[meta] Add zify plugin to META file.Emilio Jesus Gallego Arias
2019-10-23Better wording for "Show Proof" and fix typosJim Fehrle
2019-10-23Merge PR #10932: Add a notation for the empty type.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:32:57 +0000