aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarsolve.ml
Commit message (Expand)AuthorAge
* Fix lemma-overloadingGravatar Matthieu Sozeau2015-10-20
* Do occur-check w.r.t existential's types also when instantiating an evar.Gravatar Matthieu Sozeau2015-10-19
* Occur-check in evar_define was not strong enough.Gravatar Matthieu Sozeau2015-10-14
* Fix rechecking of applications: it can be given ill-typed terms. Fixes math-c...Gravatar Matthieu Sozeau2015-10-12
* Univs: Fix part of bug #4161Gravatar Matthieu Sozeau2015-10-02
* Fixing #4177 (find_projectable was liable to ask to instantiate an evar twice).Gravatar Hugo Herbelin2015-07-16
* Fixing bug #4240 (closure_of_filter was not ensuring refinement ofGravatar Hugo Herbelin2015-07-16
* 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
* 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
* 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
* 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
* 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
* 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
* Fixing 48509b61 which improved unification as expected but actuallyGravatar Hugo Herbelin2015-01-03
* Fixing #3895 (thanks to PMP for diagnosis).Gravatar Hugo Herbelin2015-01-03
* Back to the preferred ?n1:=?n2 order of evar-evar unification which got accid...Gravatar Hugo Herbelin2014-12-19
* Tentatively starting to use heuristics for evar-evar resolution: firstGravatar Hugo Herbelin2014-12-15
* Documenting check_record + changing a possibly undefined int into int option.Gravatar Hugo Herbelin2014-12-15
* Added a CannotSolveConstraint unification error and made experimentsGravatar Hugo Herbelin2014-12-11
* Tentatively more informative report of failure when inferringGravatar Hugo Herbelin2014-12-11
* Fixing orientation of postponed subtyping problems.Gravatar Hugo Herbelin2014-12-10
* Using a more aggressive test for resolving pattern equations ?n = ?p:Gravatar Hugo Herbelin2014-12-10
* Improved criterion for evar restriction in the configurationGravatar Hugo Herbelin2014-12-08
* Improving evar restriction (this is a risky change, as I remember aGravatar Hugo Herbelin2014-12-07
* Improved tracking of the origin of evars.Gravatar Hugo Herbelin2014-12-07
* Had forgotten some debugging printer.Gravatar Hugo Herbelin2014-12-07
* New approach to deal with evar-evar unification problems in differentGravatar Hugo Herbelin2014-12-04
* In solve_evar_evar, orient the heuristic over arities with differentGravatar Hugo Herbelin2014-12-03
* When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' ifGravatar Hugo Herbelin2014-12-02
* Postponing the "evar <= evar" problems instead of solving them in anGravatar Hugo Herbelin2014-12-02
* Being more scrupulous on preserving subtyping in evar-evar problems.Gravatar Hugo Herbelin2014-12-02
* Being consistent in making arbitrary choices in recursive calls toGravatar Hugo Herbelin2014-12-02
* Resolution of evar/evar problems: removed a test which should beGravatar Hugo Herbelin2014-12-02
* Fixing #3634 (wrong env in "cannot instantiate because not in itsGravatar Hugo Herbelin2014-10-03
* Work around issues with FO unification trying to unify terms ofGravatar Matthieu Sozeau2014-10-02
* Rename eq_constr functions in Evd to not break backward compatibilityGravatar Matthieu Sozeau2014-09-24
* Move the specific map_constr_with_binders_left_to_rightGravatar Matthieu Sozeau2014-09-19
* Fix constrMatching as well as change/e_contextually to allowGravatar Matthieu Sozeau2014-09-18
* Be more conservative and keep the use of eq_constr in pretyping/ functions.Gravatar Matthieu Sozeau2014-09-17
* Fix bug #3593, making constr_eq and progress work up toGravatar Matthieu Sozeau2014-09-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 16:08:19 +0000