aboutsummaryrefslogtreecommitdiff
path: root/pretyping/nativenorm.mli
AgeCommit message (Expand)Author
2020-04-06Clean and fix definitions of options.Théo Zimmermann
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-01-08Add Set NativeCompute TimingJason Gross
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-06-04Stronger invariants in unification signature.Pierre-Marie Pédrot
2018-02-27Update headers following #6543.Théo Zimmermann
2017-08-17Add native compute profiling, BZ#5170Paul Steckler
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-02-14Reductionops now return EConstrs.Pierre-Marie Pédrot
2017-02-14Nativenorm API using EConstr.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-02Reduce dependencies of interface files.Guillaume Melquiond
2015-10-15Fix #4346 1/2: native casts were not inferring universe constraints.Maxime Dénès
2015-01-12Update headers.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-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 08:07:34 +0000