| Age | Commit message (Expand) | Author |
|---|
| 2014-05-06 | Retype application of fix_proto to get the right universes in Program | Matthieu Sozeau |
| 2014-05-06 | - Fix arity handling in retyping (de Bruijn bug!) | Matthieu Sozeau |
| 2014-05-06 | Fix restrict_universe_context removing some universes that do appear in the t... | Matthieu Sozeau |
| 2014-05-06 | Fix declarations of monomorphic assumptions | Matthieu Sozeau |
| 2014-05-06 | Allow records whose sort is defined by a constant. | Matthieu Sozeau |
| 2014-05-06 | - Fix RecTutorial, and mutual induction schemes getting the wrong names. | Matthieu Sozeau |
| 2014-05-06 | Fix program Fixpoint not taking care of universes. | Matthieu Sozeau |
| 2014-05-06 | - Fixes for canonical structure resolution (check that the initial term indee... | Matthieu Sozeau |
| 2014-05-06 | Fix restrict_universe_context to not remove useful constraints. | Matthieu Sozeau |
| 2014-05-06 | - Fix eq_constr_universes restricted to Sorts.equal | Matthieu Sozeau |
| 2014-05-06 | Remove postponed constraints (unused) | Matthieu Sozeau |
| 2014-05-06 | Fixes after rebase. The use of pf_constr_of_global is problematic in presence... | 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 | Fix issue #88: restrict_universe_context was wrongly forgetting about constra... | Matthieu Sozeau |
| 2014-05-06 | Honor the Opaque flag for projections in simpl. | Matthieu Sozeau |
| 2014-05-06 | In case two constants/vars/rels are _not_ defined, force unification of unive... | Matthieu Sozeau |
| 2014-05-06 | Fix context forgetting universes (temporary, the fix is not exactly right). | Matthieu Sozeau |
| 2014-05-06 | Adapt Y. Bertot's path on private inductives (now the keyword is "Private"). | Yves Bertot |
| 2014-05-06 | - Fix abstract forgetting about new constraints. | Matthieu Sozeau |
| 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 | Fix printing of projections with implicits. | Matthieu Sozeau |
| 2014-05-06 | Fix inversion of notations for projections. | 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 | '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 |
