aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2020-02-25Merge PR #11663: Remove unqualified universe attributes.Emilio Jesus Gallego Arias
2020-02-25Merge PR #11498: [exn] Forbid raising in exn printers, make them return Pp.t ...Pierre-Marie Pédrot
2020-02-25Merge PR #11655: [parsing] Track need to reinit by typingPierre-Marie Pédrot
2020-02-24[exn] Forbid raising in exn printers, make them return Pp.t optionEmilio Jesus Gallego Arias
2020-02-23Remove unqualified universe attributes.Théo Zimmermann
2020-02-23Fix #11654: syntax of inductive declaration.Théo Zimmermann
2020-02-22Merge PR #11596: ComInductive: use lbound=Prop iff non polymorphicEmilio Jesus Gallego Arias
2020-02-22Merge PR #11635: Cleanup around the tolerability structureEmilio Jesus Gallego Arias
2020-02-22Fixing a bug introduced in PR #10832 (new format specific to a given notation).Hugo Herbelin
2020-02-22Simplification of type unparsing (index of variable in UnpMetaVar is unused).Hugo Herbelin
2020-02-22Making structure of type "tolerability" and related clearer.Hugo Herbelin
2020-02-22Preparing to simplifying the structure of type "tolerability".Hugo Herbelin
2020-02-21Merge PR #11590: Fixes #9741: only printing notations do not uselessly reserv...Emilio Jesus Gallego Arias
2020-02-21Merge PR #11642: Unconditionally print explanation for universe inconsistenciesEmilio Jesus Gallego Arias
2020-02-21[parsing] Track need to reinit by typingEmilio Jesus Gallego Arias
2020-02-21Notations: Avoiding computing parsing rule when in onlyprinting mode.Hugo Herbelin
2020-02-20Merge PR #11143: In Print/Check/Show, adopt the view that the attached type i...Emilio Jesus Gallego Arias
2020-02-20Merge PR #10832: Addressing #6082 and #7766: warning when overriding notation...Emilio Jesus Gallego Arias
2020-02-20Unconditionally print explanation for universe inconsistenciesGaëtan Gilbert
2020-02-19Merge PR #11636: Revert buggy commit mistakenly pushed with #11530Emilio Jesus Gallego Arias
2020-02-19Merge PR #11600: New syntax [Inductive Acc A R | x : Prop := ...]Emilio Jesus Gallego Arias
2020-02-19Revert "Granting #9516 and #9518 (support for numerals and strings in custom ...Hugo Herbelin
2020-02-19Addressing #6082 and #7766 (overriding format of notation).Hugo Herbelin
2020-02-19Only parsing in Reserved Notation: turning notice into a warning.Hugo Herbelin
2020-02-19ComInductive: use lbound=Prop iff non polymorphicGaëtan Gilbert
2020-02-17New syntax [Inductive Acc A R | x : Prop := ...]Gaëtan Gilbert
2020-02-17Revert "Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)"Gaëtan Gilbert
2020-02-16Revert "Suite picking numeral notation"Hugo Herbelin
2020-02-16Suite picking numeral notationHugo Herbelin
2020-02-16Granting #9516 and #9518 (support for numerals and strings in custom entries).Hugo Herbelin
2020-02-16Fixing bug #9521 (anomaly due to missing declaration of level in custom entry).Hugo Herbelin
2020-02-16Mini-factorization in vernac grammar.Hugo Herbelin
2020-02-16Custom entries: accept that no level is mentioned for a subentry.Hugo Herbelin
2020-02-15Reusing type production_level for the result of adjust_level.Hugo Herbelin
2020-02-15Reorganize type "production_level" along a more intuitive structure.Hugo Herbelin
2020-02-15Dead code in Egramcoq.adjust_level.Hugo Herbelin
2020-02-15Fixing a precedence printing bug with custom entries.Hugo Herbelin
2020-02-15Fixes #11331 (unexpected level collisions between custom entries and constr).Hugo Herbelin
2020-02-14Use thunks to univ instead of lazy constr for template typingGaëtan Gilbert
2020-02-13Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)Gaëtan Gilbert
2020-02-13Delete unused commentGaëtan Gilbert
2020-02-13Don't duplicate the inductive keyword for each block elt when parsingGaëtan Gilbert
2020-02-13Merge PR #11407: [mltop] Store digest of modules used to compile files.Gaëtan Gilbert
2020-02-13Merge PR #11521: Remove Goptions.opt_name fieldPierre-Marie Pédrot
2020-02-13Merge PR #11424: Check instance length in type_of_{inductive,constructor}Pierre-Marie Pédrot
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2020-02-12Check instance length in type_of_{inductive,constructor}Gaëtan Gilbert
2020-02-12ReferenceVariables error contains a globref instead of a constrGaëtan Gilbert
2020-02-12Merge PR #11546: Remove the Template Check option.Gaëtan Gilbert
2020-02-11Fixing some residual bugs of PR #10202 (manual implicit args in subterms).Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 07:00:05 +0000