aboutsummaryrefslogtreecommitdiff
path: root/kernel/sorts.ml
AgeCommit message (Expand)Author
2020-04-13Partial import inductive(..)Gaëtan Gilbert
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
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-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-11-06Move debug term printer to kernelMaxime Dénès
2018-06-26Remove Sorts.contentsGaëtan Gilbert
2018-02-27Update headers following #6543.Théo Zimmermann
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2016-03-22A patch renaming equal into eq in the module dealing withHugo Herbelin
2016-01-20Update copyright headers.Maxime Dénès
2015-08-02Reverting 16 last commits, committed mistakenly using the wrong push command.Hugo Herbelin
2015-08-02A patch renaming equal into eq in the module dealing withHugo Herbelin
2015-06-26Share prop/set values in sorts.ml.Matthieu Sozeau
2015-06-26BUGFIX: Three fixes for the price of 1 in sorts.ml:Matthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-12-17Ensuring the good invariants of hashcons table generation in the API.Pierre-Marie Pédrot
2014-05-06Fix extraction taking a type in the wrong environment.Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-10-24Specializing hash functions for widely used types.ppedrot
2013-10-23cList: set-as-list functions are now with an explicit comparisonletouzey
2013-08-22More complete hashcons : lists (dirpath), arrays (constr)letouzey
2013-04-29Splitting Term into five unrelated interfaces:ppedrot