aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.ml
AgeCommit message (Expand)Author
2013-02-26Names: shortcuts for building {kn, constant, mind} with empty sectionsletouzey
2013-02-18use List.rev_map whenever possibleletouzey
2013-02-11Fixing bug in native compiler with let patterns in fixpoint definitions.mdenes
2013-01-28Uniformization of the "anomaly" command.ppedrot
2013-01-28native_compute: Fixed dependencies compilation order.mdenes
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes