aboutsummaryrefslogtreecommitdiff
path: root/vernac/record.ml
AgeCommit message (Expand)Author
2019-11-26indTyping: error instead of anomaly for ill-formed templateGaëtan Gilbert
2019-11-26Fix #11039: proof of False with template poly and nonlinear universesGaëtan Gilbert
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-10-25[inductive] [declare] Move full inductive declaration to declareIndEmilio Jesus Gallego Arias
2019-09-02Merge PR #9918: Fix #9294: critical bug with template polymorphismPierre-Marie Pédrot
2019-08-27[declare] Use entry constructor instead of low-level record.Emilio Jesus Gallego Arias
2019-08-27[declare] Move proof_entry type to declare, put interactive proof data on top...Emilio Jesus Gallego Arias
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-07-01[api] Reduce declare_kinds even more.Emilio Jesus Gallego Arias
2019-07-01[declare] Separate kinds from entries in constant declarationEmilio Jesus Gallego Arias
2019-07-01[api] Refactor most of `Decl_kinds`Emilio Jesus Gallego Arias
2019-06-25Remove the internal_flag argument from Declare API.Pierre-Marie Pédrot
2019-06-24[api] Remove `polymorphic` type alias, use labels instead.Emilio Jesus Gallego Arias
2019-06-24Duplicate the type of constant entries in Proof_global.Pierre-Marie Pédrot
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-16Turning "manual_implicits" into a list of position in impargs.ml.Hugo Herbelin
2019-06-16Adding location in warning telling implicit arguments differ in term and type.Hugo Herbelin
2019-06-11Remove the side-effect role from the kernel.Pierre-Marie Pédrot
2019-06-06Merge PR #8988: Towards unifying parsing/printing for universe instances and ...Gaëtan Gilbert
2019-06-01Allowing Set to be part of universe expressions.Hugo Herbelin
2019-06-01Towards unifying parsing/printing for universe instances and Type's argument.Hugo Herbelin
2019-05-28Fix #10264: Singleton class field data is erroneous.Pierre-Marie Pédrot
2019-05-10[Canonical structures] “not_canonical” annotation to field declarationsVincent Laporte
2019-05-10[Canonical structures] Some projections may not be canonicalVincent Laporte
2019-05-07[Record] Une a record to gather field declaration attributesVincent Laporte
2019-05-07[Record] DeforestationVincent Laporte
2019-04-10Remove calls to Global.env and Libobject from RecordopsMaxime Dénès
2019-04-10Functionalize env in type classesMaxime Dénès
2019-03-30[Canonical structures] Minor refactoringVincent Laporte
2019-03-14Repair relevance marks in-kernel.Gaëtan Gilbert
2019-03-14Inductives in SProp, forbid primitive records with only sprop fieldsGaëtan Gilbert
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-03-14Make Sorts.t privateGaëtan Gilbert
2019-03-12Merge PR #9596: Fix #9595: missing non-primitive-record warning with 0 field ...Emilio Jesus Gallego Arias
2019-02-28Implement a method for manual declaration of implicits.Jasper Hugunin
2019-02-19Fix #9595: missing non-primitive-record warning with 0 field recordGaëtan Gilbert
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-02-08Merge PR #9410: Make `Program` a regular attributeMatthieu Sozeau
2019-02-05Merge PR #9373: Kernel: don't automatically downgrade ill-shaped primitive re...Pierre-Marie Pédrot
2019-02-05Make Program a regular attributeMaxime Dénès
2019-02-04Merge PR #9317: Restrict universes in records.Pierre-Marie Pédrot
2019-01-30Restrict universes in records.Gaëtan Gilbert
2019-01-25Move non-primitive-record warning to declare_mutual_inductive_with_eliminationsGaëtan Gilbert
2019-01-24Kernel: don't automatically downgrade ill-shaped primitive recordsGaëtan Gilbert
2018-12-19warn when using auto template, funind never uses template polyGaëtan Gilbert
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-11-28Merge PR #9015: [Typeclasses] Warn when RHS of `:>` is not a classMatthieu Sozeau
2018-11-27Merge PR #9046: Goptions.declare_* functions return unit instead of a write_f...Emilio Jesus Gallego Arias
2018-11-27Record.declare_class: remove unused “finite” parameterVincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:22:07 +0000