aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarsolve.ml
Commit message (Expand)AuthorAge
...
* 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
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Make evarconv and unification able to handle eta for records in presenceGravatar Matthieu Sozeau2014-08-26
* Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possibleGravatar Matthieu Sozeau2014-08-25
* Avoid introducing additional universes when doing pruning in evarsolve.Gravatar Matthieu Sozeau2014-07-30
* Missing check of evar instantiation, resulting in missing constraints (bug fr...Gravatar Matthieu Sozeau2014-07-07
* Fix a Not_found anomaly raised by solve_evar_evar, we were breaking theGravatar Matthieu Sozeau2014-07-02
* Change interface of refresh universes to get a pbty argument instead ofGravatar Matthieu Sozeau2014-06-26
* - Add an option to refresh only algebraic universes, for e_type_of. The goalGravatar Matthieu Sozeau2014-06-21
* Cleanup treatment of template universe polymorphism (thanks to E. TassiGravatar Matthieu Sozeau2014-06-20
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* Unification in HoTT_coq_061.v was looping with previous commit (whileGravatar Hugo Herbelin2014-06-16
* Fixing part of HoTT bug #61 (in declare_evar_from_virtual_equation,Gravatar Hugo Herbelin2014-06-16
* Find a more efficient fix for dealing with template universes:Gravatar Matthieu Sozeau2014-05-06
* Try a new way of handling template universe levelsGravatar Matthieu Sozeau2014-05-06
* - Fixes for canonical structure resolution (check that the initial term indee...Gravatar Matthieu Sozeau2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Better representation of evar filters: we represent the vacuous filters ofGravatar Pierre-Marie Pédrot2014-04-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 16:33:32 +0000