aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/reduction.ml
Commit message (Expand)AuthorAge
* closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Gravatar Pierre Letouzey2016-07-03
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* 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
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-02
|\
| * Fixing an incompatility introduced in a404360: kernel conversion wasGravatar Hugo Herbelin2016-04-27
* | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* | 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
* | ALPHA-CONVERSION: in the "Reduction" module: clos_fconv --> clos_gen_convGravatar Matej Kosik2015-12-17
* | ALPHA-CONVERSION: in the "Reduction" module: fconv --> gen_convGravatar Matej Kosik2015-12-17
* | 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-11-26
|\|
| * Fixing kernel bug in typing match with let-ins in the arity.Gravatar Hugo Herbelin2015-11-22
* | 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
| * Avoid dependency of the pretyper on C code.Gravatar Maxime Dénès2015-10-15
| * Fix #4346 2/2: VM casts were not inferring universe constraints.Gravatar Maxime Dénès2015-10-15
| * Fix #4346 1/2: native casts were not inferring universe constraints.Gravatar Maxime Dénès2015-10-15
| * Warn user when bytecode compilation fails.Gravatar Maxime Dénès2015-10-15
| * Remove now useless exception handler in default conversion.Gravatar Maxime Dénès2015-10-15
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-15
|\|
| * Temporary fix: kernel conversion needs to ignore l2r flag.Gravatar Maxime Dénès2015-10-14
| * 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
* | Remove dead code in lazy reduction machine.Gravatar Maxime Dénès2015-09-14
* | Output a warning when conversion compilation failed.Gravatar Maxime Dénès2015-09-06
|/
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
* Update headers.Gravatar Maxime Dénès2015-01-12
* improve efficiency of the reduction interpreter of coqtopGravatar Bruno Barras2015-01-06
* Revert commit that inverted the preference for FFlex/FProj problems inGravatar Matthieu Sozeau2014-12-10
* Option -type-in-type continued (deactivate test for inferred sort ofGravatar Hugo Herbelin2014-11-19
* Remove an ununsed pattern and commented code in the kernel.Gravatar Matthieu Sozeau2014-10-24
* Revert "Move eta-expansion after delta reduction in kernel reduction. This ma...Gravatar Matthieu Sozeau2014-10-14
* Move eta-expansion after delta reduction in kernel reduction. This makesGravatar Matthieu Sozeau2014-10-02
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Fix checker to handle projections with eta and universe polymorphism correctly.Gravatar Matthieu Sozeau2014-09-06
* Rename eta_expand_ind_stacks, fix the one from the checker and adaptGravatar Matthieu Sozeau2014-09-05
* Fix infer conv using the wrong universe conversion flexibility informationGravatar Matthieu Sozeau2014-08-03
* Cleanup code for constant equality in kernel conversion.Gravatar Matthieu Sozeau2014-07-21
* Use kernel conversion on terms that contain universe variables during unifica...Gravatar Matthieu Sozeau2014-07-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 13:12:38 +0000