aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2015-01-06Propagating the relaxing of filtering started in 48509b6, fixed inHugo Herbelin
2015-01-06Fixing old filter bug in second_order_matching.Hugo Herbelin
2015-01-03Fixing 48509b61 which improved unification as expected but actuallyHugo Herbelin
2015-01-03Tentatively trying to restore the use of second-order typed-basedHugo Herbelin
2015-01-03Fixing #3895 (thanks to PMP for diagnosis).Hugo Herbelin
2015-01-01An optimization in the use of unification candidates so as to get theHugo Herbelin
2014-12-30Simplifying second_order_matching: no need to invert the linearHugo Herbelin
2014-12-19When pretyping [uconstr] closures, don't use the local Ltac variable environm...Arnaud Spiwack
2014-12-19Back to the preferred ?n1:=?n2 order of evar-evar unification which got accid...Hugo Herbelin
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-12-16Fix for #3154: use CUnix.sys_command to call native compiler.Maxime Dénès
2014-12-15Tentatively starting to use heuristics for evar-evar resolution: firstHugo Herbelin
2014-12-15New try on Fixing an evar_map bug revealed by commit 603b66f81 onHugo Herbelin
2014-12-15Documenting check_record + changing a possibly undefined int into int option.Hugo Herbelin
2014-12-14Fix merging of name maps in union of universe contexts.Matthieu Sozeau
2014-12-12Extend the syntax of simpl with a delta flag.Arnaud Spiwack
2014-12-12Two fixes in unification (bugs #3782 and #3709)Matthieu Sozeau
2014-12-11Commit not ready. Sorry.Hugo Herbelin
2014-12-11Added a CannotSolveConstraint unification error and made experimentsHugo Herbelin
2014-12-11Fine-tuning unification error (using OccurCheck in evarconv).Hugo Herbelin
2014-12-11Tentatively more informative report of failure when inferringHugo Herbelin
2014-12-11Fixing an evar_map bug revealed by commit 603b66f81 on unification flags.Hugo 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-09Setup hook to change the unification algorithm used by evarconv,Matthieu Sozeau
2014-12-09Switch the few remaining iso-latin-1 files to utf8Pierre Letouzey
2014-12-08Fixing wrong evar_map in return clause inference, revealed by 48509b611.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-05More consistent printing of evars in evar_map debugging printer.Hugo Herbelin
2014-12-05Fix debugger Tactic Unification.Hugo Herbelin
2014-12-05Small cleaning and uniformization in unification flags:Hugo Herbelin
2014-12-04New approach to deal with evar-evar unification problems in differentHugo Herbelin
2014-12-04Occur-check in refine.Arnaud Spiwack
2014-12-04Reactivating option "Set Printing Existential Instances" for asking printing ...Hugo 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-11-27Reverting the following block of three commits:Hugo Herbelin
2014-11-26Fixing Coq compilation.Pierre-Marie Pédrot
2014-11-26Experimenting always forcing convertibility on strict implicit argumentsHugo Herbelin
2014-11-25A bit more information in debug tactic unification.Hugo Herbelin
2014-11-25Experimenting using unification when matching evar/meta free subtermsHugo Herbelin
2014-11-23Fix #3824. de Bruijn error in normalization of fixpoints.Maxime Dénès
2014-11-21Avoid compilation warning.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 15:18:14 +0000