aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Fix bug #3590, keeping evars that are not turned into named metas byGravatar Matthieu Sozeau2015-03-03
* Fix bug #4103: forgot to allow unfolding projections of cofixpoints likeGravatar Matthieu Sozeau2015-03-03
* Fix bug #4101, noccur_evar's expand_projection can legitimately failGravatar Matthieu Sozeau2015-03-03
* Fix bug introduced by my last commit, forgetting to adjust de BruijnGravatar Matthieu Sozeau2015-03-03
* Fix bug #4097.Gravatar Matthieu Sozeau2015-03-02
* Taking current env and not global env in b286c9f4f42f (4 commits ago,Gravatar Hugo Herbelin2015-02-27
* simpl: honor Global for "simpl: never" (Close: 3206)Gravatar Enrico Tassi2015-02-27
* Add support so that the type of a match in an inductive type with let-inGravatar Hugo Herbelin2015-02-27
* Fixing first part of bug #3210 (inference of pattern-matching returnGravatar Hugo Herbelin2015-02-27
* Fixing typo resulting in wrong printing of return clauses forGravatar Hugo Herbelin2015-02-27
* STM: proof state also includes meta countersGravatar Enrico Tassi2015-02-25
* Still continuing cf6a68b45, d64b5766a and 2734891ab7e on integratingGravatar Hugo Herbelin2015-02-25
* Optimizing noccur_evar wrt expansion of let-ins (fix for variant of #4076).Gravatar Hugo Herbelin2015-02-25
* An optimization on filtering evar instances with let-ins suggested byGravatar Hugo Herbelin2015-02-25
* [Proofview.tclPROGRESS]: do not consider that trivial goal instantiation is p...Gravatar Arnaud Spiwack2015-02-24
* Another bug (de Bruijn) in continuing cf6a68b45 and d64b5766a onGravatar Hugo Herbelin2015-02-24
* Compensating 6fd763431 on postponing subtyping evar-evar problems.Gravatar Hugo Herbelin2015-02-23
* Fixing cf6a68b45 on integrating ensure_evar_independent into is_constrainable...Gravatar Hugo Herbelin2015-02-23
* Fix some typos in comments.Gravatar Guillaume Melquiond2015-02-23
* Fixing rewrite/subst when the subterm to rewrite is argument of an Evar.Gravatar Hugo Herbelin2015-02-23
* Fixing occur-check which was too strong in unification.ml.Gravatar Hugo Herbelin2015-02-23
* Fixing bug #3071.Gravatar Pierre-Marie Pédrot2015-02-21
* Continuing experimentation on what part of the instance of an evarGravatar Hugo Herbelin2015-02-21
* Removing need for ensure_evar_independent by passing a force flag to is_const...Gravatar Hugo Herbelin2015-02-21
* When looking for restrictions in ?n=?p problems, keep the type of let-bindings.Gravatar Hugo Herbelin2015-02-19
* Remove some dead code and add test-suite file.Gravatar Matthieu Sozeau2015-02-16
* Fix bug #3960: potential evar instance categorized as an unresolvableGravatar Matthieu Sozeau2015-02-16
* Fix 'don't expose cases' in cbnGravatar Pierre Boutillier2015-02-15
* Fixing bug #3490.Gravatar Pierre-Marie Pédrot2015-02-15
* Fixing bug #3916.Gravatar Pierre-Marie Pédrot2015-02-15
* Univs: fix bug #3755. We were missing refreshements of universes inGravatar Matthieu Sozeau2015-02-14
* Fixing #3997 (occur-check in the presence of primitive projections, patchGravatar Hugo Herbelin2015-02-12
* Fixing bug #3900.Gravatar Pierre-Marie Pédrot2015-02-11
* Fixing #4001 (missing type constraints when building return clause of match).Gravatar Hugo Herbelin2015-02-10
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Making unification of LetIn's expressions more consistent (see #3920).Gravatar Hugo Herbelin2015-01-19
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
* Univs: Fix alias computation for VMs, computation of normal form ofGravatar Matthieu Sozeau2015-01-17
* Make native compiler handle universe polymorphic definitions.Gravatar Maxime Dénès2015-01-17
* Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
* Fix issue in printing due to de Bruijn bug when constructing compatibilityGravatar Matthieu Sozeau2015-01-13
* Update headers.Gravatar Maxime Dénès2015-01-12
* Not "Setting ?n=?p order to ?p:=?n to see if it solves someGravatar Hugo Herbelin2015-01-12
* Setting ?n=?p order to ?p:=?n to see if it solves some incompatibilities wrt ...Gravatar Hugo Herbelin2015-01-08
* Avoiding introducing yet another convention in naming files.Gravatar Hugo Herbelin2015-01-08
* Reverting the tentative try to restore the use of second-orderGravatar Hugo Herbelin2015-01-07
* Propagating the relaxing of filtering started in 48509b6, fixed inGravatar Hugo Herbelin2015-01-06
* Fixing old filter bug in second_order_matching.Gravatar Hugo Herbelin2015-01-06
* Fixing 48509b61 which improved unification as expected but actuallyGravatar Hugo Herbelin2015-01-03
* Tentatively trying to restore the use of second-order typed-basedGravatar Hugo Herbelin2015-01-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-13 01:55:05 +0000