| Commit message (Expand) | Author | Age |
|---|
| ... | |
| * | Fix extraction taking a type in the wrong environment. |  Matthieu Sozeau | 2014-05-06 |
| * | Find a more efficient fix for dealing with template universes: | Matthieu Sozeau | 2014-05-06 |
| * | Add doc on the new API for universe polymorphism and primitive projections | Matthieu Sozeau | 2014-05-06 |
| * | - Fix eq_constr_universes restricted to Sorts.equal | Matthieu Sozeau | 2014-05-06 |
| * | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau | 2014-05-06 |
| * | Adapt universe polymorphic branch to new handling of futures for delayed proofs. | Matthieu Sozeau | 2014-05-06 |
| * | Adapt Y. Bertot's path on private inductives (now the keyword is "Private"). |  Yves Bertot | 2014-05-06 |
| * | - Fix handling of polymorphic inductive elimination schemes. | Matthieu Sozeau | 2014-05-06 |
| * | Cleanup in constr, correct classification of polymorphic defs. | Matthieu Sozeau | 2014-05-06 |
| * | - Fix index-list to show computational relations for rewriting files. | Matthieu Sozeau | 2014-05-06 |
| * | Various fixes of universe polymorphism and projections when they're set. | Matthieu Sozeau | 2014-05-06 |
| * | - Fix Check to use the constraints inferred during type inference. | Matthieu Sozeau | 2014-05-06 |
| * | Improve universe/level comparison using hashes. | Matthieu Sozeau | 2014-05-06 |
| * | In kernel/univ.ml, better allocation behavior, better eq_univs function | Matthieu Sozeau | 2014-05-06 |
| * | Compat with ocaml 3.12 | Matthieu Sozeau | 2014-05-06 |
| * | - Fix comparison of universes. | Matthieu Sozeau | 2014-05-06 |
| * | Better hashconsing of levels and universes, working with modules. | Matthieu Sozeau | 2014-05-06 |
| * | Be defensive in univ/eq_instances, raise an anomaly on incompatible instances. | Matthieu Sozeau | 2014-05-06 |
| * | Reinstate hashconsing of instances, faster globally. | Matthieu Sozeau | 2014-05-06 |
| * | Restore reasonable performance by not allocating during universe checks, | Matthieu Sozeau | 2014-05-06 |
| * | - Rename eq to equal in Univ, document new modules, set interfaces. | Matthieu Sozeau | 2014-05-06 |
| * | Fix interface for template polymorphism, cleaning up code in all typing algor... | Matthieu Sozeau | 2014-05-06 |
| * | Properly reinstate old-style polymorphism in the kernel and pretyping/retyping. | Matthieu Sozeau | 2014-05-06 |
| * | Initial work on reintroducing old-style polymorphism for compatibility (the s... | Matthieu Sozeau | 2014-05-06 |
| * | Correct rebase on STM code. Thanks to E. Tassi for help on dealing with | Matthieu Sozeau | 2014-05-06 |
| * | Rework handling of universes on top of the STM, allowing for delayed | Matthieu Sozeau | 2014-05-06 |
| * | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
| * | Fixing ml-doc. |  Pierre-Marie Pédrot | 2014-05-01 |
| * | Native compiler: hide compiled files in a .coq-native subdirectory. |  Maxime Dénès | 2014-04-29 |
| * | Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to |  Hugo Herbelin | 2014-04-28 |
| * | Opaqueproofs: sink futures when interactive |  Enrico Tassi | 2014-04-25 |
| * | Fixing various backtrace recordings. | Pierre-Marie Pédrot | 2014-04-25 |
| * | Adding a [fold_map] operation on constrs. | Pierre-Marie Pédrot | 2014-04-24 |
| * | Removing dead code, thanks to new OCaml warnings and a bit of scripting. | Pierre-Marie Pédrot | 2014-04-23 |
| * | Fix guard condition for nested cofixpoints. | Maxime Dénès | 2014-04-10 |
| * | Fix exponential behavior in native compiler with retroknowledge. | Maxime Dénès | 2014-04-09 |
| * | Fix name of some Int31 operations in native compiler. | Maxime Dénès | 2014-04-09 |
| * | Optimizing Int31 support in native compiler, by not tagging | Maxime Dénès | 2014-04-09 |
| * | Int31 decompilation in native compiler was still partial. Now fixed. | Maxime Dénès | 2014-04-09 |
| * | Machine arithmetic operations for native compiler. | Maxime Dénès | 2014-04-09 |
| * | Full support for int31 values in native compiler. | Maxime Dénès | 2014-04-09 |
| * | Partial support for open terms in int31. | Maxime Dénès | 2014-04-09 |
| * | Had to split Nativelambda in two files because of Retroknowledge | Maxime Dénès | 2014-04-09 |
| * | Int31 literals in native compiler. | Maxime Dénès | 2014-04-09 |
| * | Uint31 support. | Maxime Dénès | 2014-04-09 |
| * | Fix universe handling (bug introduced in vi2vo commit) | Enrico Tassi | 2014-04-08 |
| * | Fixing coqchk. It was my fault, I misused canonical and user equalities | Pierre-Marie Pédrot | 2014-04-04 |
| * | Missing equalities in Names-like structures. | Pierre-Marie Pédrot | 2014-03-20 |
| * | Adding a Print Strategy vernacular command. It allows to check the | Pierre-Marie Pédrot | 2014-03-19 |
| * | Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it had | Pierre-Marie Pédrot | 2014-03-14 |
Matthieu Sozeau
Yves Bertot
Pierre-Marie Pédrot
Maxime Dénès
Hugo Herbelin
Enrico Tassi