index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
unification.ml
Commit message (
Expand
)
Author
Age
*
Fix #4623: set tactic too weak with universes (regression)
Maxime Dénès
2016-03-17
*
Try eta-expansion of records only on non-recursive ones
Matthieu Sozeau
2016-03-15
*
Fix strategy of Keyed Unification
Matthieu Sozeau
2016-03-09
*
Fix part of bug #4533: respect declared global transparency of
Matthieu Sozeau
2016-02-23
*
Optimizing the computation of frozen evars.
Pierre-Marie Pédrot
2016-02-03
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Extend last commit: keyed unification uses full conversions on the applied co...
Matthieu Sozeau
2016-01-12
*
Fix essential bug in new Keyed Unification mode reported by R. Krebbers.
Matthieu Sozeau
2016-01-12
*
Ensure that conversion is called on terms of the same type in
Matthieu Sozeau
2015-11-11
*
Refining 71def2f8 on too strong occur-check limiting evar-evar
Hugo Herbelin
2015-07-16
*
Safer typing primitives.
Pierre-Marie Pédrot
2015-05-13
*
Remove almost all the uses of string concatenation when building error messages.
Guillaume Melquiond
2015-04-23
*
Fixing rewrite/subst when the subterm to rewrite is argument of an Evar.
Hugo Herbelin
2015-02-23
*
Fixing occur-check which was too strong in unification.ml.
Hugo Herbelin
2015-02-23
*
Correct restriction of vm_compute when handling universe polymorphic
Matthieu Sozeau
2015-01-15
*
Update headers.
Maxime Dénès
2015-01-12
*
Simplifying second_order_matching: no need to invert the linear
Hugo Herbelin
2014-12-30
*
New try on Fixing an evar_map bug revealed by commit 603b66f81 on
Hugo Herbelin
2014-12-15
*
Documenting check_record + changing a possibly undefined int into int option.
Hugo Herbelin
2014-12-15
*
Two fixes in unification (bugs #3782 and #3709)
Matthieu Sozeau
2014-12-12
*
Commit not ready. Sorry.
Hugo Herbelin
2014-12-11
*
Fixing an evar_map bug revealed by commit 603b66f81 on unification flags.
Hugo Herbelin
2014-12-11
*
Fix debugger Tactic Unification.
Hugo Herbelin
2014-12-05
*
Small cleaning and uniformization in unification flags:
Hugo Herbelin
2014-12-05
*
Reverting the following block of three commits:
Hugo Herbelin
2014-11-27
*
Fixing Coq compilation.
Pierre-Marie Pédrot
2014-11-26
*
Experimenting always forcing convertibility on strict implicit arguments
Hugo Herbelin
2014-11-26
*
A bit more information in debug tactic unification.
Hugo Herbelin
2014-11-25
*
Experimenting using unification when matching evar/meta free subterms
Hugo Herbelin
2014-11-25
*
Option -type-in-type continued (deactivate test for inferred sort of
Hugo Herbelin
2014-11-19
*
Accepting conversion on inner closed subterms while looking for
Hugo Herbelin
2014-11-11
*
Follow up to experimental eager evar unification in bcba6d1bc9:
Hugo Herbelin
2014-11-08
*
Experimentally applying eager evar substitution at the same time as
Hugo Herbelin
2014-11-04
*
Fixing subterm matched for destruct when it is matched from prefix.
Hugo Herbelin
2014-11-02
*
Reorganization of the test for generic selection of occurrences in
Hugo Herbelin
2014-10-31
*
Enlarge the cases where the like first selection is used in destruct.
Hugo Herbelin
2014-10-31
*
Dead code
Hugo Herbelin
2014-10-27
*
Applying like-first selection for destruct in hypotheses.
Hugo Herbelin
2014-10-26
*
Fixing destruct/induction with a using clause on a non-inductive type,
Hugo Herbelin
2014-10-26
*
Dead code + typo.
Hugo Herbelin
2014-10-26
*
This commit introduces changes in induction and destruct.
Hugo Herbelin
2014-10-25
*
Reenable FO unification of primitive projections and their eta-expanded
Matthieu Sozeau
2014-10-15
*
Implement a different strategy to expand primitive projections only when
Matthieu Sozeau
2014-10-15
*
Oops, forgot a fix needed after the rebase.
Matthieu Sozeau
2014-10-14
*
Fix bug #3698: stack overflow due to eta+canonical structures in
Matthieu Sozeau
2014-10-14
*
Moving function about locs in locusops.
Hugo Herbelin
2014-10-13
*
Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name
Matthieu Sozeau
2014-10-11
*
Add a "Debug Tactic Unification" option and correct the first-order
Matthieu Sozeau
2014-10-10
*
Work around issues with FO unification trying to unify terms of
Matthieu Sozeau
2014-10-02
*
Simplify evarconv thanks to new delta status of projections,
Matthieu Sozeau
2014-09-30
[next]