aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac/taccoerce.ml
Commit message (Expand)AuthorAge
* Continuing fix to #5078, taking also into account intropatterns.Gravatar Hugo Herbelin2016-09-15
* Fixing #5078 (wrong detection of evaluable local hypotheses).Gravatar Hugo Herbelin2016-09-13
* Moving Taccoerce to ltac/ folder.Gravatar Pierre-Marie Pédrot2016-08-19