aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/reduction.mli
Commit message (Expand)AuthorAge
* Cumulativity: improve treatment of irrelevant universes.Gravatar Gaëtan Gilbert2018-03-09
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Merge PR #1082: Fixing Print for inductive types with let-in in parametersGravatar Maxime Dénès2018-02-12
|\
* | Use specialized function for inductive subtyping inference.Gravatar Gaëtan Gilbert2018-02-11
* | Simplification: cumulativity information is variance information.Gravatar Gaëtan Gilbert2018-02-10
* | [get_cumulativity_constraints] allowing further code sharing.Gravatar Gaëtan Gilbert2018-02-10
* | Factorize code for comparing maybe-cumulative inductives.Gravatar Gaëtan Gilbert2018-02-10
| * Fixing a bug of Print for inductive types with let-ins in parameters.Gravatar Hugo Herbelin2017-12-14
|/
* [api] Remove yet another type alias.Gravatar Emilio Jesus Gallego Arias2017-12-09
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
* Use inductive subtyping for conv/cumulGravatar Amin Timany2017-06-16
* Univs: fix bug #5180Gravatar Matthieu Sozeau2016-11-30
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | CLEANUP: in the Reduction moduleGravatar Matej Kosik2015-12-17
* | CLEANUP: in the Reduction moduleGravatar Matej Kosik2015-12-17
* | Unifying betazeta_applist and prod_applist into a clearer interface.Gravatar Hugo Herbelin2015-12-05
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-29
|\|
| * Conversion of polymorphic inductive types was incomplete in VM and native.Gravatar Maxime Dénès2015-10-28
* | Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-10-16
|\|
| * Remove left2right reference from the kernel.Gravatar Maxime Dénès2015-10-16
| * Fix #4346 1/2: native casts were not inferring universe constraints.Gravatar Maxime Dénès2015-10-15
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-15
|\|
| * Remove reference to default conversion function inside the kernel.Gravatar Maxime Dénès2015-10-14
* | Splitting kernel universe code in two modules.Gravatar Pierre-Marie Pédrot2015-10-06
|/
* Update headers.Gravatar Maxime Dénès2015-01-12
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Use kernel conversion on terms that contain universe variables during unifica...Gravatar Matthieu Sozeau2014-07-20
* Make kernel reduction code parametric over the handling of universes,Gravatar Matthieu Sozeau2014-06-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Support for evars and metas in native compiler.Gravatar Maxime Dénès2013-12-30
* Tentative fix of the guardedness checker by Christine and me. All stdlib and ...Gravatar Matthieu Sozeau2013-12-17
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Updating headers.Gravatar herbelin2012-08-08
* Propagated information from the reduction tactics to the kernel soGravatar herbelin2011-08-10
* - Remove create_evar_defsGravatar msozeau2011-04-13
* Starting being more explicit on the reasons why module subtyping fails.Gravatar herbelin2011-03-05
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* "Improved" the form of the inferred type of "match" byGravatar herbelin2010-06-03
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17