aboutsummaryrefslogtreecommitdiff
path: root/vernac/comInductive.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-05Fix #11048: uncaught destKO in inductive typeGaëtan Gilbert
2019-11-01minor cleanup of anonymous functionsGaëtan Gilbert
2019-11-01Expose universe processing in comInductive.Jan-Oliver Kaiser
2019-10-25[inductive] [declare] Move full inductive declaration to declareIndEmilio Jesus Gallego Arias
2019-10-24[declare] Split inductive declaration code to vernac/Emilio Jesus Gallego Arias
2019-10-24[declare] Split universe declaration code to vernac/Emilio Jesus Gallego Arias
2019-08-26Document `Template Check` flag and add changelog entry for 9918Matthieu Sozeau
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-08-08Emit Feedback.AddedAxiom in Declare instead of higher layersGaëtan Gilbert
2019-07-19[vernac] [inductive] Remove unused functions/exports.Emilio Jesus Gallego Arias
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-06-27[vernac] Cleanup on interface of VernacentriesEmilio Jesus Gallego Arias
2019-06-24[api] Remove `polymorphic` type alias, use labels instead.Emilio Jesus Gallego Arias
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-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-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-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-05Make Program a regular attributeMaxime Dénès
2019-01-25Move non-primitive-record warning to declare_mutual_inductive_with_eliminationsGaëtan Gilbert
2019-01-21Move inductive_error to Type_errorsGaëtan Gilbert
2019-01-04Default disable auto template warning.Gaë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-27Merge PR #9046: Goptions.declare_* functions return unit instead of a write_f...Emilio Jesus Gallego Arias
2018-11-26Put -indices-matter in typing_flagsGaëtan Gilbert
2018-11-23s/let _ =/let () =/ in some places (mostly goptions related)Gaëtan Gilbert
2018-11-21Make initial evar map argument to check_evars_are_solved optional.Gaëtan Gilbert
2018-11-12Only declare univ binders once for mutindGaëtan Gilbert
2018-11-09Adding universe names to polymorphic entry instances.Pierre-Marie Pédrot
2018-10-26Remove a few circumvolutions around parameters of inductive entriesMaxime Dénès
2018-10-18[api] Qualify access to `Nametab`Emilio Jesus Gallego Arias
2018-09-19Fix #7754: universe declarations on mutual inductivesGaëtan Gilbert
2018-09-13Add option to control automatic template polymorphism.Gaëtan Gilbert
2018-09-13Add explicit atribute for template polymorphism.Gaëtan Gilbert
2018-09-13Elaboration: do not ask poly inductives to be templateGaëtan Gilbert
2018-09-13Elaboration: do not ask small inductives to be templateGaëtan Gilbert
2018-09-13Small simplification of elaboration side of template poly inductivesGaëtan Gilbert
2018-07-16Restrict universes in comInductiveJasper Hugunin
2018-07-01Implement uniform parameters in ComInductiveJasper Hugunin
2018-06-26Remove Sorts.contentsGaëtan Gilbert
2018-06-18Remove reference name type.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:30:56 +0000