aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
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
* 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
* Fixing #3895 (thanks to PMP for diagnosis).Gravatar Hugo Herbelin2015-01-03
* An optimization in the use of unification candidates so as to get theGravatar Hugo Herbelin2015-01-01
* Simplifying second_order_matching: no need to invert the linearGravatar Hugo Herbelin2014-12-30
* When pretyping [uconstr] closures, don't use the local Ltac variable environm...Gravatar Arnaud Spiwack2014-12-19
* Back to the preferred ?n1:=?n2 order of evar-evar unification which got accid...Gravatar Hugo Herbelin2014-12-19
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Fix for #3154: use CUnix.sys_command to call native compiler.Gravatar Maxime Dénès2014-12-16
* Tentatively starting to use heuristics for evar-evar resolution: firstGravatar Hugo Herbelin2014-12-15
* New try on Fixing an evar_map bug revealed by commit 603b66f81 onGravatar Hugo Herbelin2014-12-15
* Documenting check_record + changing a possibly undefined int into int option.Gravatar Hugo Herbelin2014-12-15
* Fix merging of name maps in union of universe contexts.Gravatar Matthieu Sozeau2014-12-14
* Extend the syntax of simpl with a delta flag.Gravatar Arnaud Spiwack2014-12-12
* Two fixes in unification (bugs #3782 and #3709)Gravatar Matthieu Sozeau2014-12-12
* Commit not ready. Sorry.Gravatar Hugo Herbelin2014-12-11
* Added a CannotSolveConstraint unification error and made experimentsGravatar Hugo Herbelin2014-12-11
* Fine-tuning unification error (using OccurCheck in evarconv).Gravatar Hugo Herbelin2014-12-11
* Tentatively more informative report of failure when inferringGravatar Hugo Herbelin2014-12-11
* Fixing an evar_map bug revealed by commit 603b66f81 on unification flags.Gravatar 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
* Setup hook to change the unification algorithm used by evarconv,Gravatar Matthieu Sozeau2014-12-09
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
* Fixing wrong evar_map in return clause inference, revealed by 48509b611.Gravatar Hugo Herbelin2014-12-08
* 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
* More consistent printing of evars in evar_map debugging printer.Gravatar Hugo Herbelin2014-12-05
* Fix debugger Tactic Unification.Gravatar Hugo Herbelin2014-12-05
* Small cleaning and uniformization in unification flags:Gravatar Hugo Herbelin2014-12-05
* New approach to deal with evar-evar unification problems in differentGravatar Hugo Herbelin2014-12-04
* Occur-check in refine.Gravatar Arnaud Spiwack2014-12-04
* Reactivating option "Set Printing Existential Instances" for asking printing ...Gravatar 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
* Reverting the following block of three commits:Gravatar Hugo Herbelin2014-11-27
* Fixing Coq compilation.Gravatar Pierre-Marie Pédrot2014-11-26
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 15:52:44 +0000