aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.ml
AgeCommit message (Expand)Author
2016-10-03Merge remote-tracking branch 'github/pr/263' into v8.6Maxime Dénès
2016-09-09Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-09-09Tracking careless uses of slow name lookup.Pierre-Marie Pédrot
2016-09-09Restore native compiler optimizations after they were broken by 9e2ee58.Maxime Dénès
2016-09-09Packing the named_context_val in a proper record and marking it private.Pierre-Marie Pédrot
2016-09-01More efficient data structure to check if a native file is loaded.Maxime Dénès
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-19native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Pierre Letouzey
2016-05-19native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Pierre Letouzey
2016-02-15CLEANUP: Simplifying the changes done in "kernel/*"Matej Kosik
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-10-13Fix some typos.Guillaume Melquiond
2015-07-29Fixing some English misspelling.Hugo Herbelin
2015-07-10Native compiler: refactor code handling pre-computed values.Maxime Dénès
2015-06-08Fix native compilation of primitive projections. Closes #4210.Maxime Dénès
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-17Make native compiler handle universe polymorphic definitions.Maxime Dénès
2015-01-15Correct restriction of vm_compute when handling universe polymorphicMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-11-12Cleaner interfaces for linking locations of native compiler.Maxime Dénès
2014-10-24No hash consing across calls to the native compiler.Maxime Dénès
2014-10-20A patch for printing "match" when constructors are defined with let-inHugo Herbelin
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-05-01Fixing ml-doc.Pierre-Marie Pédrot
2014-04-09Fix exponential behavior in native compiler with retroknowledge.Maxime Dénès
2014-04-09Optimizing Int31 support in native compiler, by not taggingMaxime Dénès
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-04-09Int31 literals in native compiler.Maxime Dénès
2014-03-03Fixing generic hashes and replacing them with proper ones.Pierre-Marie Pédrot
2014-03-01Hunting pervasive equality in native compiler. It seems they were used forPierre-Marie Pédrot
2014-02-26Lazyconstr -> OpaqueproofEnrico Tassi
2013-12-30Support for evars and metas in native compiler.Maxime Dénès
2013-12-29Got rid of unused lazy flag in the native compiler.Maxime Dénès
2013-12-28Removing native_name reference from constant_body.Maxime Dénès
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-10-24Specializing hash functions for widely used types.ppedrot
2013-10-24Turn many List.assoc into List.assoc_fletouzey
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-07-06Fixing a bug in the native compiler, introduced by r16363, leading to undefinedmdenes
2013-04-29Merging Context and Sign.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-03-25Native compiler: hash-consing of generated code and values.mdenes
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:00:42 +0000