aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* Fix native_compute for systems with a limited size for the command line.Gravatar Guillaume Melquiond2014-05-22
* Revert "Decent error message when a constant is not found"Gravatar Enrico Tassi2014-05-16
* Decent error message when a constant is not foundGravatar Enrico Tassi2014-05-16
* Another try at close_proof that should behave better w.r.t. exception handling.Gravatar Matthieu Sozeau2014-05-16
* Rewritten the sorting algorithm for universes with a better complexity.Gravatar Pierre-Marie Pédrot2014-05-13
* Using Maps to handle imports in Safe_typing. The order is irrelevant indeed,Gravatar Pierre-Marie Pédrot2014-05-11
* Reuse universe level substitutions for template polymorphism, fixing performanceGravatar Matthieu Sozeau2014-05-09
* Avoid allocations in type_of_inductiveGravatar Matthieu Sozeau2014-05-08
* Fast-path equality of sorts in compare_constr*Gravatar Matthieu Sozeau2014-05-08
* Add missing case for primitive projection in fold_map.Gravatar Matthieu Sozeau2014-05-06
* Fix extraction taking a type in the wrong environment.Gravatar Matthieu Sozeau2014-05-06
* Find a more efficient fix for dealing with template universes:Gravatar Matthieu Sozeau2014-05-06
* Add doc on the new API for universe polymorphism and primitive projectionsGravatar Matthieu Sozeau2014-05-06
* - Fix eq_constr_universes restricted to Sorts.equalGravatar Matthieu Sozeau2014-05-06
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Adapt universe polymorphic branch to new handling of futures for delayed proofs.Gravatar Matthieu Sozeau2014-05-06
* Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Gravatar Yves Bertot2014-05-06
* - Fix handling of polymorphic inductive elimination schemes.Gravatar Matthieu Sozeau2014-05-06
* Cleanup in constr, correct classification of polymorphic defs.Gravatar Matthieu Sozeau2014-05-06
* - Fix index-list to show computational relations for rewriting files.Gravatar Matthieu Sozeau2014-05-06
* Various fixes of universe polymorphism and projections when they're set.Gravatar Matthieu Sozeau2014-05-06
* - Fix Check to use the constraints inferred during type inference.Gravatar Matthieu Sozeau2014-05-06
* Improve universe/level comparison using hashes.Gravatar Matthieu Sozeau2014-05-06
* In kernel/univ.ml, better allocation behavior, better eq_univs functionGravatar Matthieu Sozeau2014-05-06
* Compat with ocaml 3.12Gravatar Matthieu Sozeau2014-05-06
* - Fix comparison of universes.Gravatar Matthieu Sozeau2014-05-06
* Better hashconsing of levels and universes, working with modules.Gravatar Matthieu Sozeau2014-05-06
* Be defensive in univ/eq_instances, raise an anomaly on incompatible instances.Gravatar Matthieu Sozeau2014-05-06
* Reinstate hashconsing of instances, faster globally.Gravatar Matthieu Sozeau2014-05-06
* Restore reasonable performance by not allocating during universe checks,Gravatar Matthieu Sozeau2014-05-06
* - Rename eq to equal in Univ, document new modules, set interfaces.Gravatar Matthieu Sozeau2014-05-06
* Fix interface for template polymorphism, cleaning up code in all typing algor...Gravatar Matthieu Sozeau2014-05-06
* Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.Gravatar Matthieu Sozeau2014-05-06
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* Rework handling of universes on top of the STM, allowing for delayedGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Fixing ml-doc.Gravatar Pierre-Marie Pédrot2014-05-01
* Native compiler: hide compiled files in a .coq-native subdirectory.Gravatar Maxime Dénès2014-04-29
* Adding a field ci_cstr_nargs to case_info and mind_consnrealargs toGravatar Hugo Herbelin2014-04-28
* Opaqueproofs: sink futures when interactiveGravatar Enrico Tassi2014-04-25
* Fixing various backtrace recordings.Gravatar Pierre-Marie Pédrot2014-04-25
* Adding a [fold_map] operation on constrs.Gravatar Pierre-Marie Pédrot2014-04-24
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Fix guard condition for nested cofixpoints.Gravatar Maxime Dénès2014-04-10
* Fix exponential behavior in native compiler with retroknowledge.Gravatar Maxime Dénès2014-04-09
* Fix name of some Int31 operations in native compiler.Gravatar Maxime Dénès2014-04-09
* Optimizing Int31 support in native compiler, by not taggingGravatar Maxime Dénès2014-04-09
* Int31 decompilation in native compiler was still partial. Now fixed.Gravatar Maxime Dénès2014-04-09
* Machine arithmetic operations for native compiler.Gravatar Maxime Dénès2014-04-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 13:13:12 +0000