aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativeconv.ml
AgeCommit message (Expand)Author
2018-06-05More straightforward native compilation of primitive projections.Pierre-Marie Pédrot
2018-05-28Unify pre_env and envMaxime Dénès
2018-05-28Remove vm_conv hook and reorganize kernel filesMaxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-05[native_compute] Fix handling of evars in conversionMaxime Dénès
2018-02-05[native_compute] Remove useless conversion to list in reification.Maxime Dénès
2017-12-02[kernel] Patch allowing to disable VM reduction.Emilio Jesus Gallego Arias
2017-08-17Add native compute profiling, BZ#5170Paul Steckler
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-05-01More consistent writing of de Bruijn.Théo Zimmermann
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-10-28Conversion of polymorphic inductive types was incomplete in VM and native.Maxime Dénès
2015-10-15 Fix #4346 2/2: VM casts were not inferring universe constraints.Maxime Dénès
2015-10-15Fix #4346 1/2: native casts were not inferring universe constraints.Maxime Dénès
2015-07-03Fix convertibility of primitive projections for native_compute.Maxime Dénès
2015-05-14Disable precompilation for native_compute by default.Guillaume Melquiond
2015-01-17Make native compiler handle universe polymorphic definitions.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-12-16Fix for #3154: use CUnix.sys_command to call native compiler.Maxime Dénès
2014-09-13Providing a -type-in-type option for collapsing the universe hierarchy.Hugo Herbelin
2014-06-06Make kernel reduction code parametric over the handling of universes,Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-12-30Support for evars and metas in native compiler.Maxime Dénès
2013-03-05More monomorphization.ppedrot
2013-01-28Uniformization of the "anomaly" command.ppedrot
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:06:35 +0000