aboutsummaryrefslogtreecommitdiff
path: root/pretyping/inductiveops.ml
AgeCommit message (Expand)Author
2021-02-17Use make_case_or_project in auto_ind_declGaëtan Gilbert
2021-01-04Remove redundant univ and parameter info from CaseInvertGaëtan Gilbert
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
2020-12-09Adding functions to returning the def/decl status of an inductive arity.Hugo Herbelin
2020-07-01UIP in SPropGaëtan Gilbert
2020-05-12Do not use Unsafe.to_constr for old refiner conclusion.Pierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-08Ensure that template parameters are shared in the same inductive block.Pierre-Marie Pédrot
2020-02-14Use thunks to univ instead of lazy constr for template typingGaëtan Gilbert
2020-02-12ReferenceVariables error contains a globref instead of a constrGaëtan Gilbert
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-27mind_kelim is the highest allowed sort instead of a listGaëtan Gilbert
2019-04-10Remove calls to global env in InductiveopsMaxime Dénès
2019-03-14Repair relevance marks in-kernel.Gaëtan Gilbert
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-02-28Constructor type information uses the expanded form.Pierre-Marie Pédrot
2019-02-18Merge PR #9306: Remove Printing Primitive Projection CompatibilityMaxime Dénès
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-01-10Remove Printing Primitive Projection CompatibilityGaëtan Gilbert
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-11-16Termops.iter_constr_with_full_binders = EConstr.iter_with_full_bindersGaëtan Gilbert
2018-11-05Merge PR #7952: Fix an algorithmic issue in the vernac guardedness checker.Gaëtan Gilbert
2018-10-06[api] Remove (most) 8.9 deprecated objects.Emilio Jesus Gallego Arias
2018-09-26[print] Restrict use of "debug" Termops printer.Emilio Jesus Gallego Arias
2018-09-25Fix an algorithmic issue in the vernac guardedness checker.Pierre-Marie Pédrot
2018-09-23Checking if low-level name printers are used on purpose or not.Hugo Herbelin
2018-08-22Fix #8251: remove "the the" occurrencesGaëtan Gilbert
2018-07-24Projections use index representationGaëtan Gilbert
2018-06-29Merge PR #7080: Swapping Context and Constr and defining declarations on cons...Maxime Dénès
2018-06-27Swapping Context and Constr: defining declarations on constr in Constr.Hugo Herbelin
2018-06-24Handle mutual records in upper layers.Pierre-Marie Pédrot
2018-06-23Using more general information for primitive records.Pierre-Marie Pédrot
2018-06-19Merge PR #6754: Better elaboration of pattern-matchings on primitive projectionsPierre-Marie Pédrot
2018-06-17Remove the proj_body field from the kernel.Pierre-Marie Pédrot
2018-06-17Remove the proj_eta field of the kernel.Pierre-Marie Pédrot
2018-06-15Better elaboration of pattern-matchings on primitive projectionsMatthieu Sozeau
2018-05-31Reduce circular dependency constants <-> projectionsGaë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-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
2018-02-10Fix typo in Univ.CumulativityInfoGaëtan Gilbert
2017-12-23[api] Also deprecate constructors of Decl_kinds.Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-09-23Fixing _rect bug for inductive types with let-ins and non-rec uniform params.Hugo Herbelin
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-16Clean up universes of constants and inductivesAmin Timany
2017-06-16Fix a bugAmin Timany
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:59:26 +0000