aboutsummaryrefslogtreecommitdiff
path: root/pretyping/nativenorm.ml
AgeCommit message (Expand)Author
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
2015-10-15Fix #4346 1/2: native casts were not inferring universe constraints.Maxime Dénès
2015-07-10Option -type-in-type: added support in checker and making it contaminatingHugo Herbelin
2015-06-08Make normalization of primitive projections in native_compute the same as wit...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-11-23Fix #3824. de Bruijn error in normalization of fixpoints.Maxime Dénès
2014-10-22Fix missing lift in VM and native compiler (second part of #2729).Maxime Dénès
2014-10-21Porting Hugo's fix 98f3abb83a to native compiler.Maxime Dénès
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-04-09Readback for int31 values from native compiler.Maxime Dénès
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-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-03-25Native compiler: timing info for reification in debug mode.mdenes
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 12)letouzey
2013-03-12Term.dest* functions now raise specific DestKO exn instead of Invalid_argumentletouzey
2013-03-05More monomorphization.ppedrot
2013-02-28More informative error when a global reference is used in a context ofherbelin
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 10:03:23 +0000