| Age | Commit message (Expand) | Author |
|---|
| 2015-02-27 | Adding a new folder corresponding to the low-level part of the pretyper | Pierre-Marie Pédrot |
| 2015-02-02 | Removing dead code. | Pierre-Marie Pédrot |
| 2015-01-17 | Univs: proper printing of global and local universe names (only | Matthieu Sozeau |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-12-09 | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey |
| 2014-10-24 | Fixing order of hypothesis in goal hypotheses compaction for coqtop. | Hugo Herbelin |
| 2014-10-23 | Fixing order of declarations in the function which compacts variables | Hugo Herbelin |
| 2014-10-22 | Pushing Pierre's factorization of names in goal context printing from | Hugo Herbelin |
| 2014-10-20 | Fixing a (new) part of bug #2729. | Hugo Herbelin |
| 2014-09-27 | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau |
| 2014-09-19 | Use smart mapping in map_constr_with_binders_left_to_right. | Matthieu Sozeau |
| 2014-06-28 | Moved code for finding subterms (pattern, induction, set, generalize, ...) | Hugo Herbelin |
| 2014-06-28 | Extra check for indirect dependency when abstracting a term which is | Hugo Herbelin |
| 2014-06-28 | Made the subterm finding function make_abstraction independent of the | Hugo Herbelin |
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot |
| 2014-06-10 | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau |
| 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 |
