aboutsummaryrefslogtreecommitdiff
path: root/kernel/retroknowledge.mli
AgeCommit message (Expand)Author
2016-01-20Update copyright headers.Maxime Dénès
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-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-03-14Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it hadPierre-Marie Pédrot
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
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-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
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 21:02:19 +0000