aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
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
2020-11-24Merge PR #13444: Fixes another instance of bug #7967 and #8076: restriction o...coqbot-app[bot]
2020-11-23Merge PR #11841: Distinguishing entry "ident" from entry "name" in term notat...coqbot-app[bot]
2020-11-23Merge PR #13377: Fix timeout by ensuring signal exceptions are not erroneousl...Pierre-Marie Pédrot
2020-11-22Uniformizing indentation in ppvernac.ml.Hugo Herbelin
2020-11-22Renaming "ident" into "name" in grammar entries, to prevent confusions.Hugo Herbelin
2020-11-22Fixes another instance of bug #7967: restriction of universes in "Context".Hugo Herbelin
2020-11-22Fix timeout by ensuring signal exceptions are not erroneously caughtLasse Blaauwbroek
2020-11-20Add preliminary support for notations with large class (non-recursive) binders.Hugo Herbelin
2020-11-20Merge PR #13425: [stm] [declare] Try to propagate safe bits of proof informationcoqbot-app[bot]
2020-11-20Merge PR #13305: Only lower inductives to Prop if the type is syntactically a...Pierre-Marie Pédrot
2020-11-20[stm] [declare] Remove pinfo internals hack.Emilio Jesus Gallego Arias
2020-11-20[stm] [declare] Try to propagate safe bits of proof informationEmilio Jesus Gallego Arias
2020-11-18[attributes] Add output test suite for errors, improve error printing.Emilio Jesus Gallego Arias
2020-11-18[attributes] Update error message referring to deprecated syntax.Emilio Jesus Gallego Arias
2020-11-18[attributes] Deprecate `attr(true)` syntax in favor of booelan attributes.Emilio Jesus Gallego Arias
2020-11-18[attributes] Allow boolean, single-value attributes.Emilio Jesus Gallego Arias
2020-11-17Merge PR #12653: Syntax for specifying cumulative inductivescoqbot-app[bot]
2020-11-16Improve bad variance error message: mention expected and actual variancesGaëtan Gilbert
2020-11-16Merge PR #13384: Warn on hints without an explicit localitycoqbot-app[bot]
2020-11-16Merge PR #12690: Mini-fix of Locate for recursive notations using named varia...coqbot-app[bot]
2020-11-16Merge PR #13188: Default disable automatic generalization of Instance typePierre-Marie Pédrot
2020-11-16Warning on hint commands that have no explicit locality.Pierre-Marie Pédrot
2020-11-16Merge PR #13388: Export locality for all hint commandscoqbot-app[bot]
2020-11-16Only lower inductives to Prop if the type is syntactically an arity.Gaëtan Gilbert
2020-11-16Small cleanup in ComInductiveGaëtan Gilbert
2020-11-16Syntax for specifying cumulative inductivesGaëtan Gilbert
2020-11-16Infrastructure for cumulative inductive syntax (no grammar extension yet)Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:54:54 +0000