aboutsummaryrefslogtreecommitdiff
path: root/kernel/retroknowledge.mli
AgeCommit message (Expand)Author
2020-11-23Remove unused retro_reflGaëtan Gilbert
2020-07-06Primitive persistent arraysMaxime Dénès
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-11-01Implement classify on primitive floatPierre Roux
2019-11-01Change return type of primitive float comparisonPierre Roux
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
2019-11-01Declare type of primitives in CPrimitivesPierre Roux
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-03-11Remove unused Retroknowledge.Register_inlineGaëtan Gilbert
2019-02-04Primitive integersMaxime Dénès
2018-09-14Register: simpler syntaxVincent Laporte
2018-09-14Retroknowledge: use GlobRef.t instead of Constr.t as entryVincent Laporte
2018-09-14Retroknowledge: simpler parsing rulesVincent Laporte
2018-09-14Retroknowledge.KInt31: remove the (unused) group parameterVincent Laporte
2018-07-14[ltac] Remove unused functions / constructors.Emilio Jesus Gallego Arias
2018-05-28Unify pre_env and envMaxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-23New IR in VM: Clambda.Maxime Dénès
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-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 12:46:03 +0000