aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2015-03-04Merge branch 'v8.5'Pierre-Marie Pédrot
2015-03-04Fix bug #3532, providing universe inconsistency information when aMatthieu Sozeau
2015-03-03Fix bug #3590, keeping evars that are not turned into named metas byMatthieu Sozeau
2015-03-03Fix bug #4103: forgot to allow unfolding projections of cofixpoints likeMatthieu Sozeau
2015-03-03Fix bug #4101, noccur_evar's expand_projection can legitimately failMatthieu Sozeau
2015-03-03Fix bug introduced by my last commit, forgetting to adjust de BruijnMatthieu Sozeau
2015-03-02Fix bug #4097.Matthieu Sozeau
2015-02-28Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-27Taking current env and not global env in b286c9f4f42f (4 commits ago,Hugo Herbelin
2015-02-27simpl: honor Global for "simpl: never" (Close: 3206)Enrico Tassi
2015-02-27Add support so that the type of a match in an inductive type with let-inHugo Herbelin
2015-02-27Fixing first part of bug #3210 (inference of pattern-matching returnHugo Herbelin
2015-02-27Fixing typo resulting in wrong printing of return clauses forHugo Herbelin
2015-02-27Adding a new folder corresponding to the low-level part of the pretyperPierre-Marie Pédrot
2015-02-25STM: proof state also includes meta countersEnrico Tassi
2015-02-25Still continuing cf6a68b45, d64b5766a and 2734891ab7e on integratingHugo Herbelin
2015-02-25Optimizing noccur_evar wrt expansion of let-ins (fix for variant of #4076).Hugo Herbelin
2015-02-25An optimization on filtering evar instances with let-ins suggested byHugo Herbelin
2015-02-24[Proofview.tclPROGRESS]: do not consider that trivial goal instantiation is p...Arnaud Spiwack
2015-02-24Another bug (de Bruijn) in continuing cf6a68b45 and d64b5766a onHugo Herbelin
2015-02-23Compensating 6fd763431 on postponing subtyping evar-evar problems.Hugo Herbelin
2015-02-23Fixing cf6a68b45 on integrating ensure_evar_independent into is_constrainable...Hugo Herbelin
2015-02-23Fix some typos in comments.Guillaume Melquiond
2015-02-23Fixing rewrite/subst when the subterm to rewrite is argument of an Evar.Hugo Herbelin
2015-02-23Fixing occur-check which was too strong in unification.ml.Hugo Herbelin
2015-02-21Fixing bug #3071.Pierre-Marie Pédrot
2015-02-21Continuing experimentation on what part of the instance of an evarHugo Herbelin
2015-02-21Removing need for ensure_evar_independent by passing a force flag to is_const...Hugo Herbelin
2015-02-19When looking for restrictions in ?n=?p problems, keep the type of let-bindings.Hugo Herbelin
2015-02-16Remove some dead code and add test-suite file.Matthieu Sozeau
2015-02-16Fix bug #3960: potential evar instance categorized as an unresolvableMatthieu Sozeau
2015-02-15Fix 'don't expose cases' in cbnPierre Boutillier
2015-02-15Fixing bug #3490.Pierre-Marie Pédrot
2015-02-15Fixing bug #3916.Pierre-Marie Pédrot
2015-02-14Univs: fix bug #3755. We were missing refreshements of universes inMatthieu Sozeau
2015-02-12Fixing #3997 (occur-check in the presence of primitive projections, patchHugo Herbelin
2015-02-11Fixing bug #3900.Pierre-Marie Pédrot
2015-02-10Fixing #4001 (missing type constraints when building return clause of match).Hugo Herbelin
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-19Making unification of LetIn's expressions more consistent (see #3920).Hugo Herbelin
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-17Univs: Fix alias computation for VMs, computation of normal form ofMatthieu Sozeau
2015-01-17Make native compiler handle universe polymorphic definitions.Maxime Dénès
2015-01-15Correct restriction of vm_compute when handling universe polymorphicMatthieu Sozeau
2015-01-13Fix issue in printing due to de Bruijn bug when constructing compatibilityMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2015-01-12Not "Setting ?n=?p order to ?p:=?n to see if it solves someHugo Herbelin
2015-01-08Setting ?n=?p order to ?p:=?n to see if it solves some incompatibilities wrt ...Hugo Herbelin
2015-01-08Avoiding introducing yet another convention in naming files.Hugo Herbelin
2015-01-07Reverting the tentative try to restore the use of second-orderHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 16:02:43 +0000