| Age | Commit message (Expand) | Author |
|---|
| 2014-05-06 | - Fix bug preventing apply from unfolding Fixpoints. | 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 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-04-25 | Fix a second, trickier, typo in Termops.eta_reduce_head. | Arnaud Spiwack |
| 2014-04-25 | Fix a small typo in Termops.eta_reduce_head. | Arnaud Spiwack |
| 2014-02-26 | remoteCounter: backup/restore | Enrico Tassi |
| 2014-02-24 | app_node, stack, state printers | Pierre Boutillier |
| 2013-11-07 | Partial application hunt. | ppedrot |
| 2013-10-27 | Closure optimizations. | ppedrot |
| 2013-10-24 | More monomorphic List.mem + List.assoc + ... | letouzey |
| 2013-10-24 | Turn many List.assoc into List.assoc_f | letouzey |
| 2013-10-23 | cList: a few alternative to hashtbl-based uniquize, distinct, subset | letouzey |
| 2013-10-23 | cList: set-as-list functions are now with an explicit comparison | letouzey |
| 2013-10-22 | Removing some generic equalities. | ppedrot |
| 2013-09-19 | Get rid of the uses of deprecated OCaml elements (still remaining compatible ... | xclerc |
| 2013-09-18 | At least made the evar type opaque! There are still 5 remaining unsafe | ppedrot |
| 2013-08-20 | Universe counters on slaves are in sync with master | gareuselesinge |
| 2013-04-29 | Merging Context and Sign. | ppedrot |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-02-19 | avoid (Int.equal (cmp ...) 0) when a boolean equality exists | letouzey |
| 2013-02-19 | Dir_path --> DirPath | letouzey |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2012-12-19 | Array.create is deprecated | pboutill |
| 2012-12-18 | Modulification of name | ppedrot |
| 2012-12-14 | Modulification of dir_path | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-12-14 | Moved Intset and Intmap to Int namespace. | ppedrot |
| 2012-11-26 | Removed some FIXME related to equality on universes. | ppedrot |
| 2012-11-26 | Small cleaning of interface in Univ | ppedrot |
| 2012-11-22 | Monomorphization (pretyping) | ppedrot |
| 2012-11-13 | Added a CString module. | ppedrot |
| 2012-11-08 | Monomorphized a lot of equalities over OCaml integers, thanks to | ppedrot |
| 2012-09-18 | More cleaning in CArray... | ppedrot |
| 2012-09-17 | More cleaning on Utils and CList. Some parts of the code being | ppedrot |
| 2012-09-14 | As r15801: putting everything from Util.array_* to CArray.*. | ppedrot |
| 2012-09-14 | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot |
| 2012-09-14 | This patch removes unused "open" (automatically generated from | regisgia |
| 2012-09-14 | The new ocaml compiler (4.00) has a lot of very cool warnings, | regisgia |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-05-29 | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-12-17 | Reorganizing Unification.unify_0 so as to more easily share code | herbelin |
| 2011-12-06 | Backtrack on synchronizing universe counter with reset | herbelin |
| 2011-12-05 | Registering universe and meta/evar counters as summaries so as to | herbelin |
| 2011-12-04 | Fixed a small regression in pattern-matching compilation introduced in | herbelin |
| 2011-10-10 | Fixing buggy abberant code for Evarutil.expand_evar | herbelin |
| 2011-09-26 | Added support for referring to subterms of the goal by pattern. | herbelin |
| 2011-09-26 | Generalizing subst_term_occ so that it supports an arbitrary matching | herbelin |
| 2011-09-26 | Adding subst_term up to conv | herbelin |
