aboutsummaryrefslogtreecommitdiff
path: root/kernel/term.mli
AgeCommit message (Expand)Author
2019-06-17Update ml-style headers to new year.Théo Zimmermann
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
2018-06-27Swapping Context and Constr: defining declarations on constr in Constr.Hugo Herbelin
2018-06-26Remove Sorts.contentsGaëtan Gilbert
2018-05-30[api] Remove deprecated object from `Term`Emilio Jesus Gallego Arias
2018-03-28[api] Deprecate a couple of aliases that we missed.Emilio Jesus Gallego Arias
2018-03-09Allow using cumulativity without forcing strict constraints.Gaëtan Gilbert
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-12Merge PR #1082: Fixing Print for inductive types with let-in in parametersMaxime Dénès
2018-01-26Safer VM interfacesMaxime Dénès
2017-12-14Cosmetic: using "types" rather "constr" in some types of term.mli.Hugo Herbelin
2017-12-14Fixes incorrect anomaly message in lambda/prod_applist_assum + typo in doc.Hugo Herbelin
2017-11-26[api] Remove aliases of `Evar.t`Emilio Jesus Gallego Arias
2017-11-22[api] Deprecate Term destructors, move to ConstrEmilio Jesus Gallego Arias
2017-11-13[ci] [coq] Complete 4.06.0 support.Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-10Remove (useless) aliases from the API.Matej Košík
2017-05-01More consistent writing of de Bruijn.Théo Zimmermann
2017-05-01Fix for bug 5507. Mispelt de Bruijn.Théo Zimmermann
2017-03-31Make the Constr.kind_of_term type parametric in sorts and universes.Pierre-Marie Pédrot
2017-02-14Reductionops now return EConstrs.Pierre-Marie Pédrot
2016-10-31Moving unused code out of the kernel into Termops.Pierre-Marie Pédrot
2016-06-27Shrink Proofs/Obligations by default and deprecateMatthieu Sozeau
2016-02-16Term: fix a comment (first de Bruijn index is 1)Pierre Letouzey
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-12-05Unifying betazeta_applist and prod_applist into a clearer interface.Hugo Herbelin
2015-12-05Moving three related small half-general half-ad-hoc utility functionsHugo Herbelin
2015-10-19Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-18Adding a function to mirror decompose_prod_n_assum in that it counts let-ins,Hugo Herbelin
2015-10-06Splitting kernel universe code in two modules.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-12-27Revert "Term: include a function to print terms"Enrico Tassi
2014-12-26Term: include a function to print termsEnrico Tassi
2014-10-20A patch for printing "match" when constructors are defined with let-inHugo Herbelin
2014-09-30Simplify evarconv thanks to new delta status of projections,Matthieu Sozeau
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-06-10Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-28Adding a field ci_cstr_nargs to case_info and mind_consnrealargs toHugo Herbelin
2014-03-05Fix typo in comment.Maxime Dénès
2013-10-29Do not generate useless argument arrays in whd_* functions.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-04-15Checker: regroup all vo-related types in cic.mliletouzey
2013-03-25 Comments in mlipboutill
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:04:22 +0000