index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
pretyping
/
constr_matching.ml
Age
Commit message (
Expand
)
Author
2016-01-20
Update copyright headers.
Maxime Dénès
2015-10-28
Revert "Fixing #4198 (continued): not matching within the inner lambdas/let-ins"
Hugo Herbelin
2015-10-18
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-14
Fix constr_matching when a match is found in the head of a case construct
Matthieu Sozeau
2015-10-11
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-05-13
Better fixing #4198 such that the term to match is looked for before
Hugo Herbelin
2015-05-10
Code factorization in Constr_matching.
Pierre-Marie Pédrot
2015-04-21
Fixing #4198 (looking for subterms also in the return clause of match).
Hugo Herbelin
2015-03-29
Ensuring more invariants in Constr_matching.
Pierre-Marie Pédrot
2015-03-29
Fixing bug #4165.
Pierre-Marie Pédrot
2015-02-11
Fixing bug #3900.
Pierre-Marie Pédrot
2015-01-12
Update headers.
Maxime Dénès
2015-01-08
Avoiding introducing yet another convention in naming files.
Hugo Herbelin
