| Commit message (Expand) | Author | Age |
* | Fixing a bug of adjust_subst_to_rel_context. | Hugo Herbelin | 2015-11-22 |
* | Fix some typos. | Guillaume Melquiond | 2015-10-13 |
* | Assumptions: more informative print for False axiom (Close: #4054) | Enrico Tassi | 2015-06-29 |
* | Removing dead code. | Pierre-Marie Pédrot | 2015-02-02 |
* | Univs: proper printing of global and local universe names (only | Matthieu Sozeau | 2015-01-17 |
* | Update headers. | Maxime Dénès | 2015-01-12 |
* | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey | 2014-12-09 |
* | Fixing order of hypothesis in goal hypotheses compaction for coqtop. | Hugo Herbelin | 2014-10-24 |
* | Fixing order of declarations in the function which compacts variables | Hugo Herbelin | 2014-10-23 |
* | Pushing Pierre's factorization of names in goal context printing from | Hugo Herbelin | 2014-10-22 |
* | Fixing a (new) part of bug #2729. | Hugo Herbelin | 2014-10-20 |
* | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau | 2014-09-27 |
* | Use smart mapping in map_constr_with_binders_left_to_right. | Matthieu Sozeau | 2014-09-19 |
* | 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-28 |
* | Removing dead code. | Pierre-Marie Pédrot | 2014-06-17 |
* | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau | 2014-06-10 |
* | - 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-05-06 |
* | 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-04-25 |
* | remoteCounter: backup/restore | Enrico Tassi | 2014-02-26 |
* | app_node, stack, state printers | Pierre Boutillier | 2014-02-24 |
* | Partial application hunt. | ppedrot | 2013-11-07 |
* | Closure optimizations. | ppedrot | 2013-10-27 |
* | More monomorphic List.mem + List.assoc + ... | letouzey | 2013-10-24 |
* | Turn many List.assoc into List.assoc_f | letouzey | 2013-10-24 |
* | 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-23 |
* | Removing some generic equalities. | ppedrot | 2013-10-22 |
* | Get rid of the uses of deprecated OCaml elements (still remaining compatible ... | xclerc | 2013-09-19 |
* | At least made the evar type opaque! There are still 5 remaining unsafe | ppedrot | 2013-09-18 |
* | Universe counters on slaves are in sync with master | gareuselesinge | 2013-08-20 |
* | Merging Context and Sign. | ppedrot | 2013-04-29 |
* | Splitting Term into five unrelated interfaces: | ppedrot | 2013-04-29 |
* | avoid (Int.equal (cmp ...) 0) when a boolean equality exists | letouzey | 2013-02-19 |
* | Dir_path --> DirPath | letouzey | 2013-02-19 |
* | Uniformization of the "anomaly" command. | ppedrot | 2013-01-28 |
* | Array.create is deprecated | pboutill | 2012-12-19 |
* | Modulification of name | ppedrot | 2012-12-18 |
* | Modulification of dir_path | ppedrot | 2012-12-14 |
* | Modulification of identifier | ppedrot | 2012-12-14 |
* | Moved Intset and Intmap to Int namespace. | ppedrot | 2012-12-14 |
* | Removed some FIXME related to equality on universes. | ppedrot | 2012-11-26 |
* | Small cleaning of interface in Univ | ppedrot | 2012-11-26 |
* | Monomorphization (pretyping) | ppedrot | 2012-11-22 |
* | Added a CString module. | ppedrot | 2012-11-13 |