| Age | Commit message (Expand) | Author |
|---|
| 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-01 | Fixing ml-doc. | Pierre-Marie Pédrot |
| 2014-04-29 | Native compiler: hide compiled files in a .coq-native subdirectory. | Maxime Dénès |
| 2014-04-28 | Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to | Hugo Herbelin |
| 2014-04-25 | Opaqueproofs: sink futures when interactive | Enrico Tassi |
| 2014-04-25 | Fixing various backtrace recordings. | Pierre-Marie Pédrot |
| 2014-04-24 | Adding a [fold_map] operation on constrs. | Pierre-Marie Pédrot |
| 2014-04-23 | Removing dead code, thanks to new OCaml warnings and a bit of scripting. | Pierre-Marie Pédrot |
| 2014-04-10 | Fix guard condition for nested cofixpoints. | Maxime Dénès |
| 2014-04-09 | 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-08 | Fix universe handling (bug introduced in vi2vo commit) | Enrico Tassi |
| 2014-04-04 | Fixing coqchk. It was my fault, I misused canonical and user equalities | Pierre-Marie Pédrot |
| 2014-03-20 | Missing equalities in Names-like structures. | Pierre-Marie Pédrot |
| 2014-03-19 | Adding a Print Strategy vernacular command. It allows to check the | Pierre-Marie Pédrot |
| 2014-03-14 | Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it had | Pierre-Marie Pédrot |
| 2014-03-11 | vi2vo: universes handling finally fixed | Enrico Tassi |
| 2014-03-11 | Fix (3243): univ constraints of module subtyping were not propagated | Enrico Tassi |
| 2014-03-10 | Useless Array.to_list in Typeops. | Pierre-Marie Pédrot |
| 2014-03-08 | Using HMaps in global references. | Pierre-Marie Pédrot |
| 2014-03-08 | Also use HMaps in KNmap. | Pierre-Marie Pédrot |
| 2014-03-07 | Using Hashmaps by default in constant and inductive maps. This changes fold and | Pierre-Marie Pédrot |
| 2014-03-06 | Inductive maps in Environ now use HMap. | Pierre-Marie Pédrot |
| 2014-03-05 | Fix typo in comment. | Maxime Dénès |
| 2014-03-05 | Using HMaps in Safe_env.environments, hopefully improving performances. | Pierre-Marie Pédrot |
| 2014-03-05 | Canary testing absence of generic equality for KerNames | Pierre-Marie Pédrot |
| 2014-03-05 | Lazily computed hash in KerName.t. | Pierre-Marie Pédrot |
| 2014-03-05 | Remove some dead-code (thanks to ocaml warnings) | Pierre Letouzey |
| 2014-03-05 | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey |
| 2014-03-05 | Correct handling of hashconsing of constraint sets. The previous implementation | Pierre-Marie Pédrot |
| 2014-03-04 | Fixing pervasives equalities in Vconv. | Pierre-Marie Pédrot |
