aboutsummaryrefslogtreecommitdiff
path: root/kernel/retroknowledge.ml
AgeCommit message (Expand)Author
2015-01-12Update headers.Maxime Dénès
2014-10-10Fix segfault in native compiler on int31 division.Maxime Dénès
2014-09-24Make the retroknowledge marshalable.Arnaud Spiwack
2014-08-25"allows to", like "allowing to", is improperJason Gross
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-14Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it hadPierre-Marie Pédrot
2014-03-03Fixing pervasive equalities. In particular, I removed the code that deletedPierre-Marie Pédrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-11fast bitwise operations (lor,land,lxor) on int31 and BigNletouzey
2012-08-08Updating headers.herbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-05-09Added a few informations about file lineages (for the most part in kernel)herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-04-08Some dead code removal + cleanupsletouzey
2008-04-01Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientherbelin
2007-06-20ajout de head0 et tail0 en natifbgregoir
2007-05-11Processor integers + Print assumption (see coqdev mailing list for the aspiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:56:11 +0000