aboutsummaryrefslogtreecommitdiff
path: root/pretyping/unification.ml
AgeCommit message (Expand)Author
2015-05-13Safer typing primitives.Pierre-Marie Pédrot
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-02-23Fixing rewrite/subst when the subterm to rewrite is argument of an Evar.Hugo Herbelin
2015-02-23Fixing occur-check which was too strong in unification.ml.Hugo Herbelin
2015-01-15Correct restriction of vm_compute when handling universe polymorphicMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-12-30Simplifying second_order_matching: no need to invert the linearHugo 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-12Two fixes in unification (bugs #3782 and #3709)Matthieu Sozeau
2014-12-11Commit not ready. Sorry.Hugo Herbelin
2014-12-11Fixing an evar_map bug revealed by commit 603b66f81 on unification flags.Hugo Herbelin
2014-12-05Fix debugger Tactic Unification.Hugo Herbelin
2014-12-05Small cleaning and uniformization in unification flags:Hugo 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-19Option -type-in-type continued (deactivate test for inferred sort ofHugo Herbelin
2014-11-11Accepting conversion on inner closed subterms while looking forHugo Herbelin
2014-11-08Follow up to experimental eager evar unification in bcba6d1bc9:Hugo Herbelin
2014-11-04Experimentally applying eager evar substitution at the same time asHugo Herbelin
2014-11-02Fixing subterm matched for destruct when it is matched from prefix.Hugo Herbelin
2014-10-31Reorganization of the test for generic selection of occurrences inHugo Herbelin
2014-10-31Enlarge the cases where the like first selection is used in destruct.Hugo Herbelin
2014-10-27Dead codeHugo Herbelin
2014-10-26Applying like-first selection for destruct in hypotheses.Hugo Herbelin
2014-10-26Fixing destruct/induction with a using clause on a non-inductive type,Hugo Herbelin
2014-10-26Dead code + typo.Hugo Herbelin
2014-10-25This commit introduces changes in induction and destruct.Hugo Herbelin
2014-10-15Reenable FO unification of primitive projections and their eta-expandedMatthieu Sozeau
2014-10-15Implement a different strategy to expand primitive projections only whenMatthieu Sozeau
2014-10-14Oops, forgot a fix needed after the rebase.Matthieu Sozeau
2014-10-14Fix bug #3698: stack overflow due to eta+canonical structures inMatthieu Sozeau
2014-10-13Moving function about locs in locusops.Hugo Herbelin
2014-10-11Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameMatthieu Sozeau
2014-10-10Add a "Debug Tactic Unification" option and correct the first-orderMatthieu Sozeau
2014-10-02Work around issues with FO unification trying to unify terms ofMatthieu Sozeau
2014-09-30Simplify evarconv thanks to new delta status of projections,Matthieu Sozeau
2014-09-29Restoring non-uniform delta on local and global constants in 2nd orderHugo Herbelin
2014-09-29In evarconv and unification, expand folded primitive projections toMatthieu Sozeau
2014-09-27Keyed unification option, compiling the whole standard libraryMatthieu Sozeau
2014-09-27Index keys instead of simply global references.Matthieu Sozeau
2014-09-27First version of keyed subterm selection in unification.Matthieu Sozeau
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-09-24Make eq_pattern_test/eq_test work up to the equivalence of primitiveMatthieu Sozeau
2014-09-18Fix debug printing with primitive projections.Matthieu 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 13:25:48 +0000