aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evarsolve.ml
AgeCommit message (Expand)Author
2015-07-16Fixing #4177 (find_projectable was liable to ask to instantiate an evar twice).Hugo Herbelin
2015-07-16Fixing bug #4240 (closure_of_filter was not ensuring refinement ofHugo Herbelin
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-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-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-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-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-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-03Fixing 48509b61 which improved unification as expected but actuallyHugo Herbelin
2015-01-03Fixing #3895 (thanks to PMP for diagnosis).Hugo Herbelin
2014-12-19Back to the preferred ?n1:=?n2 order of evar-evar unification which got accid...Hugo Herbelin
2014-12-15Tentatively starting to use heuristics for evar-evar resolution: firstHugo Herbelin
2014-12-15Documenting check_record + changing a possibly undefined int into int option.Hugo Herbelin
2014-12-11Added a CannotSolveConstraint unification error and made experimentsHugo Herbelin
2014-12-11Tentatively more informative report of failure when inferringHugo Herbelin
2014-12-10Fixing orientation of postponed subtyping problems.Hugo Herbelin
2014-12-10Using a more aggressive test for resolving pattern equations ?n = ?p:Hugo Herbelin
2014-12-08Improved criterion for evar restriction in the configurationHugo Herbelin
2014-12-07Improving evar restriction (this is a risky change, as I remember aHugo Herbelin
2014-12-07Improved tracking of the origin of evars.Hugo Herbelin
2014-12-07Had forgotten some debugging printer.Hugo Herbelin
2014-12-04New approach to deal with evar-evar unification problems in differentHugo Herbelin
2014-12-03In solve_evar_evar, orient the heuristic over arities with differentHugo Herbelin
2014-12-02When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' ifHugo Herbelin
2014-12-02Postponing the "evar <= evar" problems instead of solving them in anHugo Herbelin
2014-12-02Being more scrupulous on preserving subtyping in evar-evar problems.Hugo Herbelin
2014-12-02Being consistent in making arbitrary choices in recursive calls toHugo Herbelin
2014-12-02Resolution of evar/evar problems: removed a test which should beHugo Herbelin
2014-10-03Fixing #3634 (wrong env in "cannot instantiate because not in itsHugo Herbelin
2014-10-02Work around issues with FO unification trying to unify terms ofMatthieu Sozeau
2014-09-24Rename eq_constr functions in Evd to not break backward compatibilityMatthieu Sozeau
2014-09-19Move the specific map_constr_with_binders_left_to_rightMatthieu Sozeau
2014-09-18Fix constrMatching as well as change/e_contextually to allowMatthieu Sozeau
2014-09-17Be more conservative and keep the use of eq_constr in pretyping/ functions.Matthieu Sozeau
2014-09-17Fix bug #3593, making constr_eq and progress work up toMatthieu Sozeau
2014-09-13Providing a -type-in-type option for collapsing the universe hierarchy.Hugo Herbelin
2014-09-12Uniformisation of the order of arguments env and sigma.Hugo Herbelin
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-08-26Make evarconv and unification able to handle eta for records in presenceMatthieu Sozeau
2014-08-25Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possibleMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 11:30:13 +0000