index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
nativecode.ml
Commit message (
Expand
)
Author
Age
*
[native_compute] Fix handling of evars in conversion
Maxime Dénès
2018-02-05
*
[native_compute] Fix evaluation of cofixpoints under primitive projections.
Maxime Dénès
2018-01-29
*
Fast environment lookup for rels.
Pierre-Marie Pédrot
2017-12-29
*
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
*
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-11-06
*
[api] Deprecate all legacy uses of Name.Id in core.
Emilio Jesus Gallego Arias
2017-11-04
*
Moving file primitive.ml to cPrimitive.ml to avoid conflict with OCaml.
Hugo Herbelin
2017-08-12
*
Safe API for accessing universe constraints of global references.
Pierre-Marie Pédrot
2017-07-11
*
Getting rid of simple calls to AUContext.instance.
Pierre-Marie Pédrot
2017-07-11
*
Removing a redundant universe instance information in native compute.
Pierre-Marie Pédrot
2017-07-10
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Clean up universes of constants and inductives
Amin Timany
2017-06-16
*
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-02
*
Remove dead code in native compiler.
Maxime Dénès
2017-05-02
*
Locally disable some warnings.
Gaetan Gilbert
2017-04-27
*
Merge branch 'v8.6' into trunk
Maxime Dénès
2017-04-15
|
\
|
*
Fix bug #5435: [Eval native_compute in] raises anomaly.
Maxime Dénès
2017-04-04
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-05
|
\
|
|
*
Merge remote-tracking branch 'github/pr/263' into v8.6
Maxime Dénès
2016-10-03
|
|
\
*
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-09-14
|
\
|
|
|
*
|
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-09-09
|
|
\
\
|
|
|
*
Tracking careless uses of slow name lookup.
Pierre-Marie Pédrot
2016-09-09
|
|
*
|
Restore native compiler optimizations after they were broken by 9e2ee58.
Maxime Dénès
2016-09-09
|
|
|
*
Packing the named_context_val in a proper record and marking it private.
Pierre-Marie Pédrot
2016-09-09
|
|
|
/
|
|
/
|
*
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-09-02
|
\
|
|
|
*
|
More efficient data structure to check if a native file is loaded.
Maxime Dénès
2016-09-01
*
|
|
CLEANUP: minor readability improvements
Matej Kosik
2016-08-24
|
/
/
*
|
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
|
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
|
*
native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)
Pierre Letouzey
2016-05-19
*
|
native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)
Pierre Letouzey
2016-05-19
*
|
CLEANUP: Simplifying the changes done in "kernel/*"
Matej Kosik
2016-02-15
*
|
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
|
/
*
Fix some typos.
Guillaume Melquiond
2015-10-13
*
Fixing some English misspelling.
Hugo Herbelin
2015-07-29
*
Native compiler: refactor code handling pre-computed values.
Maxime Dénès
2015-07-10
*
Fix native compilation of primitive projections. Closes #4210.
Maxime Dénès
2015-06-08
*
Removing dead code.
Pierre-Marie Pédrot
2015-02-02
*
Make native compiler handle universe polymorphic definitions.
Maxime Dénès
2015-01-17
*
Correct restriction of vm_compute when handling universe polymorphic
Matthieu Sozeau
2015-01-15
*
Update headers.
Maxime Dénès
2015-01-12
*
Cleaner interfaces for linking locations of native compiler.
Maxime Dénès
2014-11-12
*
No hash consing across calls to the native compiler.
Maxime Dénès
2014-10-24
*
A patch for printing "match" when constructors are defined with let-in
Hugo Herbelin
2014-10-20
*
Add a boolean to indicate the unfolding state of a primitive projection,
Matthieu Sozeau
2014-09-27
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Fixing ml-doc.
Pierre-Marie Pédrot
2014-05-01
[next]