aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2021-02-26Merge PR #13869: Use make_case_or_project in auto_ind_declPierre-Marie Pédrot
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
2020-12-09Using self-documenting argument names in two exceptions of cases.ml.Hugo Herbelin
2020-12-09Fixing support for argument scopes and let-ins while interning cases patterns.Hugo Herbelin
2020-12-07Merge PR #13556: Fix spelling in warning entrycoqbot-app[bot]
2020-12-06Add support for high resolution timeout functions.Lasse Blaauwbroek
2020-12-06Fix spelling in warning entrySimon Friis Vindum
2020-12-04Merge PR #13552: Delay inventing names for monomorphic universesPierre-Marie Pédrot
2020-12-04Delay inventing names for monomorphic universesGaëtan Gilbert
2020-12-02Move *_with_full_binders variants out of the kernel.Pierre-Marie Pédrot
2020-11-27Merge PR #12586: [declare] Allow custom typing flags when declaring constants.coqbot-app[bot]
2020-11-27Merge PR #13483: Fix #13283: improved error on `clear implicit` flagcoqbot-app[bot]
2020-11-27Fix #13283: improved error on `clear implicit` flagFabian Kunze
2020-11-26[attributes] [typing] Rename `typing` to `bypass_check`Emilio Jesus Gallego Arias
2020-11-26[environ] [typing_flags] Introduce helper function to remove duplicate codeEmilio Jesus Gallego Arias
2020-11-26[proofs] Support per-definition typing-flags in interactive proofs.Emilio Jesus Gallego Arias
2020-11-26[vernac] Allow to control typing flags with attributes.Emilio Jesus Gallego Arias
2020-11-26[kernel] Allow to set typing flags in add_constantEmilio Jesus Gallego Arias
2020-11-26[declare] Allow custom typing flags when declaring constants.Emilio Jesus Gallego Arias
2020-11-26Merge PR #13415: Separate interning and pretyping of universescoqbot-app[bot]
2020-11-25Separate interning and pretyping of universesGaëtan Gilbert
2020-11-25Reserve "sort_expr" for uninterned universesGaëtan Gilbert
2020-11-24Add a new evar source to refer to evars which are types of evars.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 01:33:14 +0000