aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
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
2014-11-20Probably useless use of a global-environment reading function in Indrec.Pierre-Marie Pédrot
2014-11-19Making map_union a standard function of the ML library.Hugo Herbelin
2014-11-19Option -type-in-type continued (deactivate test for inferred sort ofHugo Herbelin
2014-11-19Continuing fixing nested but convertible occurrences in find_subtermHugo Herbelin
2014-11-19Printing function for [uconstr].Arnaud Spiwack
2014-11-19uconstr: fix bug in interpretation of Ltac-bound name in let-tuple and patter...Arnaud Spiwack
2014-11-19Glob-ops: a name-mapping operation for pattern-matching binders.Arnaud Spiwack
2014-11-18Fixing a little bug with nested but convertible occurrences in "destruct at".Hugo Herbelin
2014-11-18Fixing detection of occurrences in the presence of nested subterms forHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 03:30:46 +0000