aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2021-04-23Merge PR #13965: [abbreviation] user syntax to set interp scope of argumentPierre-Marie Pédrot
2021-04-18Merge PR #14112: Cleanup useless environment manipulation in Class declarationcoqbot-app[bot]
2021-04-14Cleanup useless environment manipulation in Class declarationGaëtan Gilbert
2021-04-14Remove remote counter systemGaëtan Gilbert
2021-04-14Put async worker id in universe namesGaëtan Gilbert
2021-04-07[abbreviation] allow the user to set arguments scopeEnrico Tassi
2021-04-07cleanup: less exceptions, removal of try_interp_name_aliasEnrico Tassi
2021-04-06Missing dot in an error message.Hugo Herbelin
2021-04-06One catch-all's missing a noncritical; another is now useless (see 7efaf86).Hugo Herbelin
2021-04-06Uniformizing the "already exists" messagesHugo Herbelin
2021-03-26[recordops] complete API rewrite; the module is now called [structures]Enrico Tassi
2021-03-25Merge PR #13852: [vernac] Improve alpha-renaming in record projection typescoqbot-app[bot]
2021-03-24Mention label name in signature mismatch error when constant expectedGaëtan Gilbert
2021-03-10Merge PR #13840: [notation] option to fine tune printing of literalscoqbot-app[bot]
2021-03-09Add the source and target classes to the coercion tableKazuhiko Sakaguchi
2021-03-09Replace cl_index with cl_typ in coercionops.mlKazuhiko Sakaguchi
2021-03-06[vernac] Improve alpha-renaming in record projection typesLi-yao Xia
2021-03-04[notation] option to fine tune printing of literalsEnrico Tassi
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
2021-02-28Merge PR #13853: Delay the dynamic linking of native-code libraries until nat...Pierre-Marie Pédrot
2021-02-26Merge PR #13869: Use make_case_or_project in auto_ind_declPierre-Marie Pédrot
2021-02-26Delay the dynamic linking of native-code libraries until native_compute is ca...Guillaume Melquiond
2021-02-25[proof using] Remove duplicate code, refactor.Emilio Jesus Gallego Arias
2021-02-24Infrastructure for fine-grained debug flagsMaxime Dénès
2021-02-17Use make_case_or_project in auto_ind_declGaëtan Gilbert
2021-02-17Reduce imperative arrays in build_beq_scheme + reindentGaëtan Gilbert
2021-02-17Merge PR #13734: Fix #13732: Implicit Type vs universesPierre-Marie Pédrot
2021-02-11Merge PR #13844: [vernac] pass the loc of the whole command to the interp fun...coqbot-app[bot]
2021-02-11[vernac] pass the loc of the whole command to the interp functionEnrico Tassi
2021-02-04Remove deprecated -sprop-cumulative command line argumentGaëtan Gilbert
2021-01-28vernac/declaremods: make object collection tail-recursiveGabriel Scherer
2021-01-28Merge PR #13763: Remove the SearchHead command (deprecated in 8.12)coqbot-app[bot]
2021-01-28Merge PR #13790: [vernac] Check that no proofs do remain open at section/modu...coqbot-app[bot]
2021-01-27[vernac] move vernac_classifier to vernacEnrico Tassi
2021-01-26[vernac] Check that no proofs do remain open at section/module closing timeEmilio Jesus Gallego Arias
2021-01-26Merge PR #13758: Remove the Hide Obligations flag (deprecated in 8.12)coqbot-app[bot]
2021-01-25Remove the SearchHead commandJim Fehrle
2021-01-25Remove the Hide Obligations flagJim Fehrle
2021-01-20Merge PR #13744: Make sure "Print Module" write a dot at the end of inductive...coqbot-app[bot]
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
2021-01-14Merge PR #13378: Add support for high resolution timeout functionsPierre-Marie Pédrot
2021-01-13Make sure "Print Module" write a dot at the end of inductive definitions.Guillaume Melquiond
2021-01-11Do not declare a global universe object when the universe set is empty.Pierre-Marie Pédrot
2021-01-11Fix #13732: Implicit Type vs universesGaëtan Gilbert
2021-01-09Merge PR #13299: Remember universe instances of constants in notationscoqbot-app[bot]
2021-01-07Merge PR #13718: Move printing and sorting out of AcyclicGraphcoqbot-app[bot]
2021-01-06Further pushing up the printing and sorting of universes.Pierre-Marie Pédrot
2021-01-04Remember universe instances of constants in notationsJasper Hugunin
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
2020-12-21Move evaluable_global_reference from Names to Tacred.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:49:32 +0000