aboutsummaryrefslogtreecommitdiff
path: root/pretyping/nativenorm.ml
AgeCommit message (Expand)Author
2020-11-09Remove the native symbol registering from the safe environment.Pierre-Marie Pédrot
2020-07-11Merge PR #12646: Correctly readback blocked CaseInvert matches in VM/nativePierre-Marie Pédrot
2020-07-06Correctly readback blocked CaseInvert matches in VM/nativeGaëtan Gilbert
2020-07-06Primitive persistent arraysMaxime Dénès
2020-07-01UIP in SPropGaëtan Gilbert
2020-04-21Merge PR #11896: Use lists instead of arrays in evar instances.Maxime Dénès
2020-04-16NativeCompute Timing: Use real, not user timeJason Gross
2020-04-06Clean and fix definitions of options.Théo Zimmermann
2020-04-06Use lists instead of arrays in evar instances.Pierre-Marie Pédrot
2020-04-01Merge PR #11306: Centralize the flag handling native compilation.Maxime Dénès
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-01-08Add Set NativeCompute TimingJason Gross
2019-12-22Centralize the flag handling native compilation.Pierre-Marie Pédrot
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-01Add primitive floats to 'native_compute'Pierre Roux
2019-07-04Merge PR #10359: Remove dependency of native_compile on global env for symbolsMaxime Dénès
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-12Remove dependency of native_compile on global env for symbolsGaëtan Gilbert
2019-04-29Fix variant of #9344 for native_computeMaxime Dénès
2019-04-16Better error message when OCaml compiler not found for native computeMaxime Dénès
2019-04-05[native compiler] Normalize before destructuring sortMaxime Dénès
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-02-28Constructor type information uses the expanded form.Pierre-Marie Pédrot
2019-02-04Primitive integersMaxime Dénès
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-10-09Fix nativenorm when an evar is in the wrong place.Gaëtan Gilbert
2018-09-14Retroknowledge: use GlobRef.t instead of Constr.t as entryVincent Laporte
2018-07-26Fix #8121: anomalies in native_compute with let and evars.Pierre-Marie Pédrot
2018-07-24Projections use index representationGaëtan Gilbert
2018-07-03Merge PR #7607: Simplify reification of predicate in bytecode and native comp...Pierre-Marie Pédrot
2018-06-28Deprecate Environ.retroknowledge function in favor of the projectionGaëtan Gilbert
2018-06-28Simplify reification of predicate in bytecode and native compilersMaxime Dénès
2018-06-23Using more general information for primitive records.Pierre-Marie Pédrot
2018-06-05Merge PR #7679: Clean native compilation of primitive projectionsMaxime Dénès
2018-06-05More straightforward native compilation of primitive projections.Pierre-Marie Pédrot
2018-06-04Preserving "canonical" form of return predicate in native_compute.Hugo Herbelin
2018-05-28Unify pre_env and envMaxime Dénès
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
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-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-04[api] Deprecate all legacy uses of Name.Id in core.Emilio Jesus Gallego Arias
2017-09-29Remove some duplication between Typeops and Nativenorm.Gaëtan Gilbert
2017-08-22use OCaml 4.03-compatible Filename functionsPaul Steckler
2017-08-18use OCaml temp_file, instead of our own versionPaul Steckler
2017-08-18move filename search to start_profilerPaul Steckler
2017-08-17Add native compute profiling, BZ#5170Paul Steckler
2017-07-04Bump year in headers.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:05:44 +0000