index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
retroknowledge.ml
Commit message (
Expand
)
Author
Age
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Remove (useless) aliases from the API.
Matej Košík
2017-06-10
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Update headers.
Maxime Dénès
2015-01-12
*
Fix segfault in native compiler on int31 division.
Maxime Dénès
2014-10-10
*
Make the retroknowledge marshalable.
Arnaud Spiwack
2014-09-24
*
"allows to", like "allowing to", is improper
Jason Gross
2014-08-25
*
Machine arithmetic operations for native compiler.
Maxime Dénès
2014-04-09
*
Full support for int31 values in native compiler.
Maxime Dénès
2014-04-09
*
Partial support for open terms in int31.
Maxime Dénès
2014-04-09
*
Had to split Nativelambda in two files because of Retroknowledge
Maxime Dénès
2014-04-09
*
Int31 literals in native compiler.
Maxime Dénès
2014-04-09
*
Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it had
Pierre-Marie Pédrot
2014-03-14
*
Fixing pervasive equalities. In particular, I removed the code that deleted
Pierre-Marie Pédrot
2014-03-03
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
fast bitwise operations (lor,land,lxor) on int31 and BigN
letouzey
2012-08-11
*
Updating headers.
herbelin
2012-08-08
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Added a few informations about file lineages (for the most part in kernel)
herbelin
2010-05-09
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Some dead code removal + cleanups
letouzey
2009-04-08
*
Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient
herbelin
2008-04-01
*
ajout de head0 et tail0 en natif
bgregoir
2007-06-20
*
Processor integers + Print assumption (see coqdev mailing list for the
aspiwack
2007-05-11