aboutsummaryrefslogtreecommitdiff
path: root/vernac/comInductive.ml
AgeCommit message (Expand)Author
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
2018-06-04[econstr] Remove some Unsafe.to_constr use.Emilio Jesus Gallego Arias
2018-05-31[api] Move `Constrexpr` to the `interp` module.Emilio Jesus Gallego Arias
2018-05-25Remove some occurrences of Evd.emptyMaxime Dénès
2018-05-22Merge PR #7384: Split UniversesPierre-Marie Pédrot
2018-05-17Remove unused argument to solve_constraints_systemGaëtan Gilbert
2018-05-17Move solve_constraint_system near its only use site (comInductive)Gaëtan Gilbert
2018-05-08[api] Move universe syntax to `Glob_term`Emilio Jesus Gallego Arias
2018-04-17Deprecate mixing univ minimization and evm normalization functions.Gaëtan Gilbert
2018-04-12Fixing the 3 cases of a "Stream.Error" ended with two periods.Hugo Herbelin
2018-03-09[located] Push inner locations in `reference` to a CAst.t node.Emilio Jesus Gallego Arias
2018-03-07Merge PR #6790: Allow universe declarations for [with Definition].Maxime Dénès
2018-03-05Allow universe declarations for [with Definition].Gaëtan Gilbert
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-02-28[econstr] Continue consolidation of EConstr API under `interp`.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2018-02-11Use specialized function for inductive subtyping inference.Gaëtan Gilbert
2018-02-10Inference of inductive subtyping does not need an evar map.Gaëtan Gilbert
2018-02-10Simplification: cumulativity information is variance information.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:39:03 +0000