| Commit message (Expand) | Author | Age |
* | Ensuring more invariants in Constr_matching. | Pierre-Marie Pédrot | 2015-03-29 |
* | Fixing bug #4165. | Pierre-Marie Pédrot | 2015-03-29 |
* | use a more compact representation of non-constant constructors | Benjamin Gregoire | 2015-03-27 |
* | Fix bug 4157, | Benjamin Gregoire | 2015-03-26 |
* | 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-25 |
* | Fixing equality of notation_constrs. Fixes bug #4136. | Pierre-Marie Pédrot | 2015-03-24 |
* | Add function to fix the non-substituted universe variables of an evar_map. | Matthieu Sozeau | 2015-03-17 |
* | Fix bug #3532, providing universe inconsistency information when a | Matthieu Sozeau | 2015-03-04 |
* | 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-03 |
* | Fix bug #4097. | Matthieu Sozeau | 2015-03-02 |
* | 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-27 |
* | 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-25 |
* | [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-24 |
* | 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-23 |
* | 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-21 |
* | When looking for restrictions in ?n=?p problems, keep the type of let-bindings. | Hugo Herbelin | 2015-02-19 |
* | 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-16 |
* | 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-15 |
* | Univs: fix bug #3755. We were missing refreshements of universes in | Matthieu Sozeau | 2015-02-14 |
* | Fixing #3997 (occur-check in the presence of primitive projections, patch | Hugo Herbelin | 2015-02-12 |
* | Fixing bug #3900. | Pierre-Marie Pédrot | 2015-02-11 |
* | Fixing #4001 (missing type constraints when building return clause of match). | Hugo Herbelin | 2015-02-10 |
* | Removing dead code. | Pierre-Marie Pédrot | 2015-02-02 |
* | Making unification of LetIn's expressions more consistent (see #3920). | Hugo Herbelin | 2015-01-19 |
* | 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-17 |
* | Correct restriction of vm_compute when handling universe polymorphic | Matthieu Sozeau | 2015-01-15 |
* | Fix issue in printing due to de Bruijn bug when constructing compatibility | Matthieu Sozeau | 2015-01-13 |