aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.mli
AgeCommit message (Expand)Author
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-09Optimizing Int31 support in native compiler, by not taggingMaxime Dénès
2014-04-09Int31 decompilation in native compiler was still partial. Now fixed.Maxime Dénès
2014-04-09Machine arithmetic operations for native compiler.Maxime Dénès
2014-04-09Full support for int31 values in native compiler.Maxime Dénès
2014-04-09Partial support for open terms in int31.Maxime Dénès
2014-04-09Had to split Nativelambda in two files because of RetroknowledgeMaxime Dénès
2014-04-09Int31 literals in native compiler.Maxime Dénès
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-12-30Support for evars and metas in native compiler.Maxime Dénès
2013-03-25Native compiler: hash-consing of generated code and values.mdenes
2013-02-11Fixing bug in native compiler with let patterns in fixpoint definitions.mdenes
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:08:47 +0000