| Age | Commit message (Expand) | Author |
|---|
| 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 | 'Pretty' printer for wf_paths | Pierre |
| 2014-05-06 | md5 for MacOS | Pierre |
| 2014-05-06 | Lemmas: export standard proof terminator | Enrico Tassi |
| 2014-05-06 | Rewriting the proof monad mechanism. Now it uses pure OCaml code, without | ppedrot |
| 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-05 | Fix install target in Makefile after 6acf543800fe176ca7d47ef7165ebc14588efb6f. | Maxime Dénès |
| 2014-05-02 | Pos.iter arguments in a better order for cbn. | Pierre Boutillier |
| 2014-05-02 | Cbn is happier when ?SetPositive fixpoints have the set as recursive argument | Pierre Boutillier |
| 2014-05-02 | Eta contractions to please cbn | Pierre Boutillier |
| 2014-05-02 | Update test-suite Makefile to handle coq-prog-args | Jason Gross |
| 2014-05-01 | Allowing the "Declare Instance" command anywhere. This was artificially | Pierre-Marie Pédrot |
| 2014-05-01 | Fixing ml-doc. | Pierre-Marie Pédrot |
| 2014-04-30 | Fix Qcanon after changes on injection. | Maxime Dénès |
| 2014-04-30 | Document changes on injection. | Maxime Dénès |
| 2014-04-30 | Trying to improve the error messages of injection. | Maxime Dénès |
| 2014-04-29 | Injection: do not fail when arguments have sort Prop. | Maxime Dénès |
| 2014-04-29 | Native compiler: hide compiled files in a .coq-native subdirectory. | Maxime Dénès |
| 2014-04-29 | Completing 5eb53b5bc8d765ed75e965f43f1084e18efc8790 (I unfortunately | Hugo Herbelin |
| 2014-04-28 | Reduce the amount of "Coq <" prompts generated by coq_tex. (Partial fix for b... | Guillaume Melquiond |
| 2014-04-28 | Prevent coq_tex from generating curly quotes. (Partial fix for bug #2964) | Guillaume Melquiond |
| 2014-04-28 | Recognize Parameters as a command in coqdoc. (Fix for bug #3279) | Guillaume Melquiond |
| 2014-04-28 | Mark lazymatch as an Ltac keyword for coqdoc. (Fix for bug #3276) | Guillaume Melquiond |
| 2014-04-28 | Remove unused lookup table. | Guillaume Melquiond |
| 2014-04-28 | Fix broken commit 2bcb2cb. | Guillaume Melquiond |
| 2014-04-28 | Fix incorrect syntax highlighting after the Goal command. | Guillaume Melquiond |
| 2014-04-28 | Fixing coqdoc bug #3292 (unfortunate collision betweens the relative | Hugo Herbelin |
| 2014-04-28 | Fixing #3293 (eta-expansion at "match" printing time was failing | Hugo Herbelin |
| 2014-04-28 | Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to | Hugo Herbelin |
| 2014-04-27 | Rewriting [lapply] tactic in the new monad. | Pierre-Marie Pédrot |
| 2014-04-27 | Giving true proof-terms in inversion instead of metas. | Pierre-Marie Pédrot |
| 2014-04-25 | coq_makefile: -I for the new stm/ dir | Enrico Tassi |
| 2014-04-25 | Adding a stm/ folder, as asked during last workgroup. It was essentially moving | Pierre-Marie Pédrot |
| 2014-04-25 | Removing Autoinstance once and for all. | Pierre-Marie Pédrot |
| 2014-04-25 | Removing useless try-with clauses in Goal.enter variants. | Pierre-Marie Pédrot |
| 2014-04-25 | Future: memory optimization when forcing a chained pure computation | Enrico Tassi |
| 2014-04-25 | Opaqueproofs: sink futures when interactive | Enrico Tassi |
