| Age | Commit message (Expand) | Author |
|---|
| 2015-03-27 | use a more compact representation of non-constant constructors | Benjamin Gregoire |
| 2015-03-26 | Fix bug 4157, | Benjamin Gregoire |
| 2015-03-25 | Fully fixing bug #3491 (anomaly when building _rect scheme in the | Hugo Herbelin |
| 2015-03-25 | Use kernel names instead of user names when looking for coercions. (Fix for b... | Guillaume Melquiond |
| 2015-03-24 | Fixing equality of notation_constrs. Fixes bug #4136. | Pierre-Marie Pédrot |
| 2015-03-17 | Add function to fix the non-substituted universe variables of an evar_map. | Matthieu Sozeau |
| 2015-03-04 | Fix bug #3532, providing universe inconsistency information when a | Matthieu Sozeau |
| 2015-03-03 | Fix bug #3590, keeping evars that are not turned into named metas by | Matthieu Sozeau |
| 2015-03-03 | Fix bug #4103: forgot to allow unfolding projections of cofixpoints like | Matthieu Sozeau |
| 2015-03-03 | Fix bug #4101, noccur_evar's expand_projection can legitimately fail | Matthieu Sozeau |
| 2015-03-03 | Fix bug introduced by my last commit, forgetting to adjust de Bruijn | Matthieu Sozeau |
| 2015-03-02 | Fix bug #4097. | Matthieu Sozeau |
| 2015-02-27 | Taking current env and not global env in b286c9f4f42f (4 commits ago, | Hugo Herbelin |
| 2015-02-27 | simpl: honor Global for "simpl: never" (Close: 3206) | Enrico Tassi |
| 2015-02-27 | Add support so that the type of a match in an inductive type with let-in | Hugo Herbelin |
| 2015-02-27 | Fixing first part of bug #3210 (inference of pattern-matching return | Hugo Herbelin |
| 2015-02-27 | Fixing typo resulting in wrong printing of return clauses for | Hugo Herbelin |
| 2015-02-25 | STM: proof state also includes meta counters | Enrico Tassi |
| 2015-02-25 | Still continuing cf6a68b45, d64b5766a and 2734891ab7e on integrating | Hugo Herbelin |
| 2015-02-25 | Optimizing noccur_evar wrt expansion of let-ins (fix for variant of #4076). | Hugo Herbelin |
| 2015-02-25 | An optimization on filtering evar instances with let-ins suggested by | Hugo Herbelin |
| 2015-02-24 | [Proofview.tclPROGRESS]: do not consider that trivial goal instantiation is p... | Arnaud Spiwack |
| 2015-02-24 | Another bug (de Bruijn) in continuing cf6a68b45 and d64b5766a on | Hugo Herbelin |
| 2015-02-23 | Compensating 6fd763431 on postponing subtyping evar-evar problems. | Hugo Herbelin |
| 2015-02-23 | Fixing cf6a68b45 on integrating ensure_evar_independent into is_constrainable... | Hugo Herbelin |
| 2015-02-23 | Fix some typos in comments. | Guillaume Melquiond |
| 2015-02-23 | Fixing rewrite/subst when the subterm to rewrite is argument of an Evar. | Hugo Herbelin |
| 2015-02-23 | Fixing occur-check which was too strong in unification.ml. | Hugo Herbelin |
| 2015-02-21 | Fixing bug #3071. | Pierre-Marie Pédrot |
| 2015-02-21 | Continuing experimentation on what part of the instance of an evar | Hugo Herbelin |
| 2015-02-21 | Removing need for ensure_evar_independent by passing a force flag to is_const... | Hugo Herbelin |
| 2015-02-19 | When looking for restrictions in ?n=?p problems, keep the type of let-bindings. | Hugo Herbelin |
| 2015-02-16 | Remove some dead code and add test-suite file. | Matthieu Sozeau |
| 2015-02-16 | Fix bug #3960: potential evar instance categorized as an unresolvable | Matthieu Sozeau |
| 2015-02-15 | Fix 'don't expose cases' in cbn | Pierre Boutillier |
| 2015-02-15 | Fixing bug #3490. | Pierre-Marie Pédrot |
| 2015-02-15 | Fixing bug #3916. | Pierre-Marie Pédrot |
| 2015-02-14 | Univs: fix bug #3755. We were missing refreshements of universes in | Matthieu Sozeau |
| 2015-02-12 | Fixing #3997 (occur-check in the presence of primitive projections, patch | Hugo Herbelin |
| 2015-02-11 | Fixing bug #3900. | Pierre-Marie Pédrot |
| 2015-02-10 | Fixing #4001 (missing type constraints when building return clause of match). | Hugo Herbelin |
| 2015-02-02 | Removing dead code. | Pierre-Marie Pédrot |
| 2015-01-19 | Making unification of LetIn's expressions more consistent (see #3920). | Hugo Herbelin |
| 2015-01-17 | Univs: proper printing of global and local universe names (only | Matthieu Sozeau |
| 2015-01-17 | Univs: Fix alias computation for VMs, computation of normal form of | Matthieu Sozeau |
| 2015-01-17 | Make native compiler handle universe polymorphic definitions. | Maxime Dénès |
| 2015-01-15 | Correct restriction of vm_compute when handling universe polymorphic | Matthieu Sozeau |
| 2015-01-13 | Fix issue in printing due to de Bruijn bug when constructing compatibility | Matthieu Sozeau |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2015-01-12 | Not "Setting ?n=?p order to ?p:=?n to see if it solves some | Hugo Herbelin |
