| Age | Commit message (Expand) | Author |
|---|
| 2014-06-21 | - Add an option to refresh only algebraic universes, for e_type_of. The goal | Matthieu Sozeau |
| 2014-06-20 | Cleanup treatment of template universe polymorphism (thanks to E. Tassi | Matthieu Sozeau |
| 2014-05-09 | Refresh universes for Ltac's type_of, as the term can be used anywhere, | 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 | 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-03-05 | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey |
| 2013-10-24 | More monomorphic List.mem + List.assoc + ... | letouzey |
| 2013-05-14 | Delayed the computation of parameters in sort polymorphism of | herbelin |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-02-17 | A more informative message when the elimination predicate for | herbelin |
| 2013-02-10 | Moved code from Pretype_error to Evarutil | ppedrot |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2012-12-18 | Taking into account the possibility of having a type of type which is | herbelin |
| 2012-11-22 | Monomorphization (pretyping) | 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-03-02 | Noise for nothing | pboutill |
| 2011-11-21 | Renamig support added to "Arguments" | gareuselesinge |
| 2011-10-25 | Still more unification in typing.ml | herbelin |
| 2011-10-24 | More unification in type_of and addition of e_type_of to get the new | herbelin |
| 2011-10-11 | Unification in the return clause of match was not supported in solve_evars. | herbelin |
| 2011-10-10 | Applied the trick of Chung-Kil Hur to solve second-order matching | herbelin |
| 2011-10-05 | It happens that the type inference algorithm (pretyping) did not check | herbelin |
| 2011-04-08 | Replaced printing number of ill-typed branch by printing name of constructor | herbelin |
| 2010-09-24 | Some dead code removal, thanks to Oug analyzer | letouzey |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-05 | Added a function in typing.ml to solve evars of a constr w/o going back down ... | herbelin |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-07-07 | Jolification : tentative de supprimer les "( evd)" et associés qui | aspiwack |
| 2009-02-19 | On remplace evar_map par evar_defs (seul evar_defs est désormais exporté | aspiwack |
| 2008-04-13 | Bugs, nettoyage, et améliorations diverses | herbelin |
| 2008-03-15 | Application de refresh_universes dans typing.ml et retyping.ml : les | herbelin |
| 2007-08-27 | Suppression des type_app et body_of_type qui alourdissent inutilement le code | herbelin |
| 2007-06-07 | Unification des types + clause filtrage manquante + uniformisation locale | herbelin |
| 2007-01-22 | Correction pour le rapport de bug #1325 par rétablissement du | herbelin |
| 2006-10-28 | Extension du polymorphisme de sorte au cas des définitions dans Type. | herbelin |
| 2006-05-28 | - Indtypes: en attente opinion CoRN, les occurrences de Type non explicites | herbelin |
| 2006-05-23 | Nouvelle implantation du polymorphisme de sorte pour les familles inductives | herbelin |
| 2006-03-29 | Inductifs avec polymorphisme de sorte (version initiale) | herbelin |
| 2005-12-02 | Changement des named_context | gregoire |
| 2005-06-06 | essai de typage des instantiations d\'evars | barras |
| 2005-01-14 | Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed | sacerdot |
| 2004-09-17 | restructuration des printers: proofs passe avant parsing | barras |
| 2004-09-15 | hiding the meta_map in evar_defs | barras |
| 2004-09-03 | premiere reorganisation de l\'unification | barras |
