aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
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
2020-11-15Merge PR #12611: [record] Cleanup of data structure and functionscoqbot-app[bot]
2020-11-15Moving the analysis of notation strings in notation.ml.Hugo Herbelin
2020-11-15Implement export locality for the remaining Hint commands.Pierre-Marie Pédrot
2020-11-15Default disable automatic generalization of Instance typeGaëtan Gilbert
2020-11-13[record] Some documentation + minor refactoringEmilio Jesus Gallego Arias
2020-11-13[record] [ci] Overlay for elpiEmilio Jesus Gallego Arias
2020-11-13[record] Options API cleanup.Emilio Jesus Gallego Arias
2020-11-13[record] Refactor nested functions.Emilio Jesus Gallego Arias
2020-11-13[record] Cleanup of data structure and functions [2/2]Emilio Jesus Gallego Arias
2020-11-13[record] Cleanup of data structure and functions [1/2]Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 04:42:45 +0000