| Age | Commit message (Expand) | Author |
|---|
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2015-10-18 | Miscellaneous typos, spacing, US spelling in comments or variable names. | Hugo Herbelin |
| 2015-10-15 | Fix #4346 2/2: VM casts were not inferring universe constraints. | Maxime Dénès |
| 2015-10-15 | Fix #4346 1/2: native casts were not inferring universe constraints. | Maxime Dénès |
| 2015-10-12 | Univs: be more restrictive for template polymorphic constants: only | Matthieu Sozeau |
| 2015-07-10 | Option -type-in-type: added support in checker and making it contaminating | Hugo Herbelin |
| 2015-02-10 | Fix typeops ignoring results of check functions with let _, and one | Matthieu Sozeau |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-09-27 | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau |
| 2014-08-28 | Change the way primitive projections are declared to the kernel. | Matthieu Sozeau |
| 2014-08-03 | Move to a representation of universe polymorphic constants using indices for ... | Matthieu Sozeau |
| 2014-06-28 | Quickly fixing bug #2996: typing functions now check when referring to | Hugo Herbelin |
| 2014-06-04 | - Fix hashing of levels to get the "right" order in universe contexts etc... | Matthieu Sozeau |
| 2014-05-09 | Reuse universe level substitutions for template polymorphism, fixing performance | 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 | 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-10 | Useless Array.to_list in Typeops. | Pierre-Marie Pédrot |
| 2013-12-30 | Support for evars and metas in native compiler. | Maxime Dénès |
| 2013-05-14 | Delayed the computation of parameters in sort polymorphism of | herbelin |
| 2013-04-29 | Merging Context and Sign. | ppedrot |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-02-28 | More informative error when a global reference is used in a context of | herbelin |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2013-01-22 | New implementation of the conversion test, using normalization by evaluation to | mdenes |
| 2012-11-22 | Monomorphization (kernel) | ppedrot |
| 2012-09-14 | As r15801: putting everything from Util.array_* to CArray.*. | 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-09-24 | Completing r14448 and thus continuing r14407 (using Cast to propagate | herbelin |
| 2011-09-04 | Having added a special Cast for remembering the use of conversion | herbelin |
| 2011-08-10 | Propagated information from the reduction tactics to the kernel so | herbelin |
| 2011-07-29 | Term_typing, Typeops: replace some generic '=' on constr by eq_constr | puech |
| 2011-04-13 | Revert "Add [Polymorphic] flag for defs" | msozeau |
| 2011-04-13 | Add [Polymorphic] flag for defs | msozeau |
| 2011-04-08 | Replaced printing number of ill-typed branch by printing name of constructor | herbelin |
| 2010-12-18 | Univ.constraints made fully abstract instead of being a Set of abstract stuff | letouzey |
| 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 |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2008-04-30 | Réutilisation de l'infrastructure pour le polymorphisme d'univers des | herbelin |
| 2008-04-27 | Correction du bug des types singletons pas sous-type de Set | herbelin |
| 2007-08-27 | Suppression des type_app et body_of_type qui alourdissent inutilement le code | herbelin |
| 2006-10-29 | Compatibilité du polymorphisme de constantes avec les sections. | herbelin |
| 2006-10-28 | Extension du polymorphisme de sorte au cas des définitions dans Type. | herbelin |
