index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
kernel
/
nativecode.ml
Age
Commit message (
Expand
)
Author
2015-02-02
Removing dead code.
Pierre-Marie Pédrot
2015-01-17
Make native compiler handle universe polymorphic definitions.
Maxime Dénès
2015-01-15
Correct restriction of vm_compute when handling universe polymorphic
Matthieu Sozeau
2015-01-12
Update headers.
Maxime Dénès
2014-11-12
Cleaner interfaces for linking locations of native compiler.
Maxime Dénès
2014-10-24
No hash consing across calls to the native compiler.
Maxime Dénès
2014-10-20
A patch for printing "match" when constructors are defined with let-in
Hugo Herbelin
2014-09-27
Add a boolean to indicate the unfolding state of a primitive projection,
Matthieu Sozeau
2014-05-06
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-01
Fixing ml-doc.
Pierre-Marie Pédrot
2014-04-09
Fix exponential behavior in native compiler with retroknowledge.
Maxime Dénès
2014-04-09
Optimizing Int31 support in native compiler, by not tagging
Maxime Dénès
2014-04-09
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-03-03
Fixing generic hashes and replacing them with proper ones.
Pierre-Marie Pédrot
2014-03-01
Hunting pervasive equality in native compiler. It seems they were used for
Pierre-Marie Pédrot
2014-02-26
Lazyconstr -> Opaqueproof
Enrico Tassi
2013-12-30
Support for evars and metas in native compiler.
Maxime Dénès
2013-12-29
Got rid of unused lazy flag in the native compiler.
Maxime Dénès
2013-12-28
Removing native_name reference from constant_body.
Maxime Dénès
2013-10-24
More monomorphic List.mem + List.assoc + ...
letouzey
2013-10-24
Specializing hash functions for widely used types.
ppedrot
2013-10-24
Turn many List.assoc into List.assoc_f
letouzey
2013-09-27
Removing a bunch of generic equalities.
ppedrot
2013-07-06
Fixing a bug in the native compiler, introduced by r16363, leading to undefined
mdenes
2013-04-29
Merging Context and Sign.
ppedrot
2013-04-29
Splitting Term into five unrelated interfaces:
ppedrot
2013-03-25
Native compiler: hash-consing of generated code and values.
mdenes
2013-03-25
Native compiler: Inlined constants are now compiled, fixing a bug reported by
mdenes
2013-03-13
Restrict (try...with...) to avoid catching critical exn (part 8)
letouzey
2013-03-12
invalid_arg instead of raise (Invalid_argement ...)
letouzey
2013-03-05
More monomorphization.
ppedrot
2013-02-26
kernel/declarations becomes a pure mli
letouzey
2013-02-26
Names: shortcuts for building {kn, constant, mind} with empty sections
letouzey
2013-02-18
use List.rev_map whenever possible
letouzey
2013-02-11
Fixing bug in native compiler with let patterns in fixpoint definitions.
mdenes
2013-01-28
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
native_compute: Fixed dependencies compilation order.
mdenes
2013-01-22
New implementation of the conversion test, using normalization by evaluation to
mdenes
