aboutsummaryrefslogtreecommitdiff
path: root/pretyping/retyping.ml
AgeCommit message (Expand)Author
2021-03-30[flags] [profile] Remove bit-rotten CProfile code.Emilio Jesus Gallego Arias
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
2020-11-16Extend hack to use postponed constraints in retyping to template polyGaëtan Gilbert
2020-07-08Merge PR #12627: Fix Canonical with universe polymorphism and primitive proje...Enrico Tassi
2020-07-06Primitive persistent arraysMaxime Dénès
2020-07-05Fix Canonical with universe polymorphism and primitive projectionGaëtan Gilbert
2020-07-01UIP in SPropGaëtan Gilbert
2020-05-10No more local reduction functions in Reductionops.Pierre-Marie Pédrot
2020-03-28Remove some cruft from Reductionops API.Pierre-Marie Pédrot
2020-03-18Rename Retypeops -> RelevanceopsGaëtan Gilbert
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-14Use thunks to univ instead of lazy constr for template typingGaëtan Gilbert
2019-11-22Use the relevance flag in CClosure rel contexts in an efficient way.Pierre-Marie Pédrot
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-04-10Remove calls to global env in InductiveopsMaxime Dénès
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-03-14Make Sorts.t privateGaëtan Gilbert
2019-02-04Primitive integersMaxime Dénès
2018-10-31Renaming is_template_polymorphic -> is_template_polymorphic_ind.Hugo Herbelin
2018-06-26Remove Sorts.contentsGaëtan Gilbert
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-03-31[econstr] Forbid calling `to_constr` in open terms.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2017-12-09[lib] Rename Profile to CProfileEmilio Jesus Gallego Arias
2017-11-28Adding a variant get_truncation_family_of of get_sort_family_of.Hugo Herbelin
2017-11-28Moving non-recursive function sort_family_of out of the retype block of recur...Hugo Herbelin
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-09-28Remove trivial TODO comment (constants can't be template poly now).Gaëtan Gilbert
2017-07-26Removing template polymorphism for definitions.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-04-01Using delayed universe instances in EConstr.Pierre-Marie Pédrot
2017-04-01Actually exporting delayed universes in the EConstr implementation.Pierre-Marie Pédrot
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
2017-02-14Removing compatibility layers in RetypingPierre-Marie Pédrot
2017-02-14Reductionops now return EConstrs.Pierre-Marie Pédrot
2017-02-14Eliminating parts of the right-hand side compatibility layerPierre-Marie Pédrot
2017-02-14Leminv API using EConstr.Pierre-Marie Pédrot
2017-02-14Cleaning up opening of the EConstr module in pretyping folder.Pierre-Marie Pédrot
2017-02-14Making judgment type generic over the type of inner constrs.Pierre-Marie Pédrot
2017-02-14Retyping API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops API using EConstr.Pierre-Marie Pédrot
2017-02-14Termops API using EConstr.Pierre-Marie Pédrot
2016-08-24CLEANUP: minor readability improvementsMatej Kosik
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:06:11 +0000