index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
constr_matching.ml
Commit message (
Expand
)
Author
Age
*
Revert "Fixing #4198 (continued): not matching within the inner lambdas/let-ins"
Hugo Herbelin
2015-10-28
*
Fixing #4198 (continued): not matching within the inner lambdas/let-ins
Hugo Herbelin
2015-10-18
*
Using appropriate lambda decomposition function counting let-ins when
Hugo Herbelin
2015-10-18
*
Fix constr_matching when a match is found in the head of a case construct
Matthieu Sozeau
2015-10-14
*
Fixing untimely unexpected warning "Collision between bound variables" (#4317).
Hugo Herbelin
2015-10-11
*
Constr_matching: renaming misleading name stk into ctx.
Hugo Herbelin
2015-10-11
*
Better fixing #4198 such that the term to match is looked for before
Hugo Herbelin
2015-05-13
*
Code factorization in Constr_matching.
Pierre-Marie Pédrot
2015-05-10
*
Fixing #4198 (looking for subterms also in the return clause of match).
Hugo Herbelin
2015-04-21
*
Ensuring more invariants in Constr_matching.
Pierre-Marie Pédrot
2015-03-29
*
Fixing bug #4165.
Pierre-Marie Pédrot
2015-03-29
*
Fixing bug #3900.
Pierre-Marie Pédrot
2015-02-11
*
Update headers.
Maxime Dénès
2015-01-12
*
Avoiding introducing yet another convention in naming files.
Hugo Herbelin
2015-01-08