aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/unification.ml
Commit message (Expand)AuthorAge
...
* Fixing rewrite/subst when the subterm to rewrite is argument of an Evar.Gravatar Hugo Herbelin2015-02-23
* Fixing occur-check which was too strong in unification.ml.Gravatar Hugo Herbelin2015-02-23
* Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
* Update headers.Gravatar Maxime Dénès2015-01-12
* Simplifying second_order_matching: no need to invert the linearGravatar Hugo Herbelin2014-12-30
* 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
* Two fixes in unification (bugs #3782 and #3709)Gravatar Matthieu Sozeau2014-12-12
* Commit not ready. Sorry.Gravatar Hugo Herbelin2014-12-11
* Fixing an evar_map bug revealed by commit 603b66f81 on unification flags.Gravatar Hugo Herbelin2014-12-11
* Fix debugger Tactic Unification.Gravatar Hugo Herbelin2014-12-05
* Small cleaning and uniformization in unification flags:Gravatar Hugo Herbelin2014-12-05
* Reverting the following block of three commits:Gravatar Hugo Herbelin2014-11-27
* Fixing Coq compilation.Gravatar Pierre-Marie Pédrot2014-11-26
* Experimenting always forcing convertibility on strict implicit argumentsGravatar Hugo Herbelin2014-11-26
* A bit more information in debug tactic unification.Gravatar Hugo Herbelin2014-11-25
* Experimenting using unification when matching evar/meta free subtermsGravatar Hugo Herbelin2014-11-25
* Option -type-in-type continued (deactivate test for inferred sort ofGravatar Hugo Herbelin2014-11-19
* Accepting conversion on inner closed subterms while looking forGravatar Hugo Herbelin2014-11-11
* Follow up to experimental eager evar unification in bcba6d1bc9:Gravatar Hugo Herbelin2014-11-08
* Experimentally applying eager evar substitution at the same time asGravatar Hugo Herbelin2014-11-04
* Fixing subterm matched for destruct when it is matched from prefix.Gravatar Hugo Herbelin2014-11-02
* Reorganization of the test for generic selection of occurrences inGravatar Hugo Herbelin2014-10-31
* Enlarge the cases where the like first selection is used in destruct.Gravatar Hugo Herbelin2014-10-31
* Dead codeGravatar Hugo Herbelin2014-10-27
* Applying like-first selection for destruct in hypotheses.Gravatar Hugo Herbelin2014-10-26
* Fixing destruct/induction with a using clause on a non-inductive type,Gravatar Hugo Herbelin2014-10-26
* Dead code + typo.Gravatar Hugo Herbelin2014-10-26
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Reenable FO unification of primitive projections and their eta-expandedGravatar Matthieu Sozeau2014-10-15
* Implement a different strategy to expand primitive projections only whenGravatar Matthieu Sozeau2014-10-15
* Oops, forgot a fix needed after the rebase.Gravatar Matthieu Sozeau2014-10-14
* Fix bug #3698: stack overflow due to eta+canonical structures inGravatar Matthieu Sozeau2014-10-14
* Moving function about locs in locusops.Gravatar Hugo Herbelin2014-10-13
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* Add a "Debug Tactic Unification" option and correct the first-orderGravatar Matthieu Sozeau2014-10-10
* Work around issues with FO unification trying to unify terms ofGravatar Matthieu Sozeau2014-10-02
* Simplify evarconv thanks to new delta status of projections,Gravatar Matthieu Sozeau2014-09-30
* Restoring non-uniform delta on local and global constants in 2nd orderGravatar Hugo Herbelin2014-09-29
* In evarconv and unification, expand folded primitive projections toGravatar Matthieu Sozeau2014-09-29
* Keyed unification option, compiling the whole standard libraryGravatar Matthieu Sozeau2014-09-27
* Index keys instead of simply global references.Gravatar Matthieu Sozeau2014-09-27
* First version of keyed subterm selection in unification.Gravatar Matthieu Sozeau2014-09-27
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Make eq_pattern_test/eq_test work up to the equivalence of primitiveGravatar Matthieu Sozeau2014-09-24
* Fix debug printing with primitive projections.Gravatar 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
* Fix bug #3610, allowing betaiotadelta reduction while unifying types ofGravatar Matthieu Sozeau2014-09-15
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-21 15:23:10 +0000