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
...
*
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
*
Restoring non-uniform delta on local and global constants in 2nd order
Hugo Herbelin
2014-09-29
*
In evarconv and unification, expand folded primitive projections to
Matthieu Sozeau
2014-09-29
*
Keyed unification option, compiling the whole standard library
Matthieu Sozeau
2014-09-27
*
Index keys instead of simply global references.
Matthieu Sozeau
2014-09-27
*
First version of keyed subterm selection in unification.
Matthieu Sozeau
2014-09-27
*
Add a boolean to indicate the unfolding state of a primitive projection,
Matthieu Sozeau
2014-09-27
*
Make eq_pattern_test/eq_test work up to the equivalence of primitive
Matthieu Sozeau
2014-09-24
*
Fix debug printing with primitive projections.
Matthieu Sozeau
2014-09-18
*
Be more conservative and keep the use of eq_constr in pretyping/ functions.
Matthieu Sozeau
2014-09-17
*
Fix bug #3593, making constr_eq and progress work up to
Matthieu Sozeau
2014-09-17
*
Fix bug #3610, allowing betaiotadelta reduction while unifying types of
Matthieu Sozeau
2014-09-15
*
Providing a -type-in-type option for collapsing the universe hierarchy.
Hugo Herbelin
2014-09-13
*
Uniformisation of the order of arguments env and sigma.
Hugo Herbelin
2014-09-12
*
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-09-12
*
Fix bug #3505.
Matthieu Sozeau
2014-09-11
*
A step towards better differentiating when w_unify is used for subterm
Hugo Herbelin
2014-09-10
*
Print [Variant] types with the keyword [Variant].
Arnaud Spiwack
2014-09-04
*
Change the way primitive projections are declared to the kernel.
Matthieu Sozeau
2014-08-28
*
Fix bugs #3484 and #3546.
Matthieu Sozeau
2014-08-28
[prev]
[next]