| Age | Commit message (Expand) | Author |
|---|
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2015-11-25 | Reverting 1467c225 (Fixing an old typo in Retyping, found by Matej). | Hugo Herbelin |
| 2015-11-24 | Fixing an old typo in Retyping, found by Matej. | Hugo Herbelin |
| 2015-07-09 | Make retyping of projections more resilient to wrong environment. | Maxime Dénès |
| 2015-07-05 | Fix handling of primitive projections in VM. | Maxime Dénès |
| 2015-02-27 | Taking current env and not global env in b286c9f4f42f (4 commits ago, | Hugo Herbelin |
| 2015-02-27 | Add support so that the type of a match in an inductive type with let-in | Hugo Herbelin |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-10-02 | Work around issues with FO unification trying to unify terms of | Matthieu Sozeau |
| 2014-10-01 | Fixing use of arguments renaming in apply which was broken after | Hugo Herbelin |
| 2014-09-27 | Make pattern_of_constr typed so that we can infer the proper patterns | Matthieu Sozeau |
| 2014-09-27 | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau |
| 2014-09-18 | Fix constrMatching as well as change/e_contextually to allow | Matthieu Sozeau |
| 2014-09-18 | Fix debug printing with primitive projections. | Matthieu Sozeau |
| 2014-06-28 | Quickly fixing bug #2996: typing functions now check when referring to | Hugo Herbelin |
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot |
| 2014-06-01 | Use of "H"-based names for propositional hypotheses obtained by | Hugo Herbelin |
| 2014-05-06 | - Fix arity handling in retyping (de Bruijn bug!) | Matthieu Sozeau |
| 2014-05-06 | Allow records whose sort is defined by a constant. | 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-04-23 | Removing dead code, thanks to new OCaml warnings and a bit of scripting. | Pierre-Marie Pédrot |
| 2013-09-19 | Get rid of the uses of deprecated OCaml elements (still remaining compatible ... | xclerc |
| 2013-07-19 | - Fix uncaught exception NotASort from reductionops, moving decomp_sort to re... | msozeau |
| 2013-05-14 | Delayed the computation of parameters in sort polymorphism of | herbelin |
| 2013-05-05 | Hack to solve a "Bad recursive type" anomaly. | herbelin |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-03-17 | Retyping.get_type_of: a lax version raising no anomalies | letouzey |
| 2013-02-05 | Fixed bug #2981 (anomaly NotASort in Retyping due to collision between | herbelin |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-11-22 | Monomorphization (pretyping) | ppedrot |
| 2012-09-14 | Partial revert of Yann commit in order to use CLib.List when opening | ppedrot |
| 2012-09-14 | This patch removes unused "open" (automatically generated from | regisgia |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-07-04 | Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml | letouzey |
| 2011-04-11 | Catch NotArity exception and transform it into an anomaly in retyping. | msozeau |
| 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 |
| 2009-05-23 | A try at using sort variables during unification. Instead of refreshing | msozeau |
| 2009-04-08 | - Fixing bug #2084 (unification not checking sort constraints), hoping | herbelin |
| 2009-03-04 | Backtrack sur la mémoïsation de nf_evar. | aspiwack |
| 2009-02-27 | =?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=... | aspiwack |
| 2009-02-06 | pushed evar reduction in kernel | barras |
| 2009-01-12 | Fix a bunch of bugs related to setoid_rewrite, unification and evars: | msozeau |
| 2008-12-28 | - Another bug in get_sort_family_of (sort-polymorphism of constants and | herbelin |
