aboutsummaryrefslogtreecommitdiff
path: root/pretyping/nativenorm.ml
AgeCommit message (Expand)Author
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
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-06-02Don't double up on periods in anomaliesJason Gross
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-02-14Reductionops now return EConstrs.Pierre-Marie Pédrot
2017-02-14Inv API using EConstr.Pierre-Marie Pédrot
2017-02-14Pretyping API using EConstr.Pierre-Marie Pédrot
2017-02-14Nativenorm API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops API using EConstr.Pierre-Marie Pédrot
2016-08-30CLEANUP: using |> operator more consistentlyMatej Kosik
2016-08-24CLEANUP: minor readability improvementsMatej Kosik
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-20Update copyright headers.Maxime Dénès
2015-10-28Fix bug in native compiler with universe polymorphism.Maxime Dénès
2015-10-15 Fix #4346 2/2: VM casts were not inferring universe constraints.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-13 18:15:02 +0000