| Commit message (Expand) | Author | Age |
|---|
| * | Update copyright headers. |  Maxime Dénès | 2016-01-20 |
| * | (Partial) fix for bug #4453: raise an error instead of an anomaly. |  Matthieu Sozeau | 2015-12-17 |
| * | Safer typing primitives. |  Pierre-Marie Pédrot | 2015-05-13 |
| * | Update headers. | Maxime Dénès | 2015-01-12 |
| * | Fixing a bug in the presence of let-in in inductive arity. |  Hugo Herbelin | 2014-10-20 |
| * | Providing a -type-in-type option for collapsing the universe hierarchy. | Hugo Herbelin | 2014-09-13 |
| * | Proofview refiner is now type-safe by default. | Pierre-Marie Pédrot | 2014-09-04 |
| * | Typing.sort_of does not leak evarmaps anymore. | Pierre-Marie Pédrot | 2014-09-04 |
| * | A tentative uniform naming policy in module Inductiveops. | Hugo Herbelin | 2014-08-01 |
| * | Quickly fixing bug #2996: typing functions now check when referring to | Hugo Herbelin | 2014-06-28 |
| * | Change interface of refresh universes to get a pbty argument instead of | Matthieu Sozeau | 2014-06-26 |
| * | - Add an option to refresh only algebraic universes, for e_type_of. The goal |  Matthieu Sozeau | 2014-06-21 |
| * | Cleanup treatment of template universe polymorphism (thanks to E. Tassi | Matthieu Sozeau | 2014-06-20 |
| * | Refresh universes for Ltac's type_of, as the term can be used anywhere, | Matthieu Sozeau | 2014-05-09 |
| * | - 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 |
| * | Initial work on reintroducing old-style polymorphism for compatibility (the s... | Matthieu Sozeau | 2014-05-06 |
| * | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
| * | Remove many superfluous 'open' indicated by ocamlc -w +33 |  Pierre Letouzey | 2014-03-05 |
| * | More monomorphic List.mem + List.assoc + ... |  letouzey | 2013-10-24 |
| * | Delayed the computation of parameters in sort polymorphism of |  herbelin | 2013-05-14 |
| * | Splitting Term into five unrelated interfaces: |  ppedrot | 2013-04-29 |
| * | A more informative message when the elimination predicate for | herbelin | 2013-02-17 |
| * | Moved code from Pretype_error to Evarutil | ppedrot | 2013-02-10 |
| * | Uniformization of the "anomaly" command. | ppedrot | 2013-01-28 |
| * | Taking into account the possibility of having a type of type which is | herbelin | 2012-12-18 |
| * | Monomorphization (pretyping) | ppedrot | 2012-11-22 |
| * | 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-09-14 |
| * | Updating headers. | herbelin | 2012-08-08 |
| * | Noise for nothing |  pboutill | 2012-03-02 |
| * | Renamig support added to "Arguments" |  gareuselesinge | 2011-11-21 |
| * | Still more unification in typing.ml | herbelin | 2011-10-25 |
| * | More unification in type_of and addition of e_type_of to get the new | herbelin | 2011-10-24 |
| * | Unification in the return clause of match was not supported in solve_evars. | herbelin | 2011-10-11 |
| * | Applied the trick of Chung-Kil Hur to solve second-order matching | herbelin | 2011-10-10 |
| * | It happens that the type inference algorithm (pretyping) did not check | herbelin | 2011-10-05 |
| * | Replaced printing number of ill-typed branch by printing name of constructor | herbelin | 2011-04-08 |
| * | Some dead code removal, thanks to Oug analyzer | letouzey | 2010-09-24 |
| * | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
| * | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
| * | Added a function in typing.ml to solve evars of a constr w/o going back down ... | herbelin | 2010-04-05 |
| * | Delete trailing whitespaces in all *.{v,ml*} files |  glondu | 2009-09-17 |
| * | Jolification : tentative de supprimer les "( evd)" et associés qui |  aspiwack | 2009-07-07 |
| * | On remplace evar_map par evar_defs (seul evar_defs est désormais exporté | aspiwack | 2009-02-19 |
| * | Bugs, nettoyage, et améliorations diverses | herbelin | 2008-04-13 |
| * | Application de refresh_universes dans typing.ml et retyping.ml : les | herbelin | 2008-03-15 |
| * | Suppression des type_app et body_of_type qui alourdissent inutilement le code | herbelin | 2007-08-27 |
| * | Unification des types + clause filtrage manquante + uniformisation locale | herbelin | 2007-06-07 |
Maxime Dénès
Matthieu Sozeau
Pierre-Marie Pédrot
Hugo Herbelin
Matthieu Sozeau
Pierre Letouzey
letouzey
herbelin
ppedrot
regisgia
pboutill
gareuselesinge
glondu
aspiwack