diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-23 22:47:38 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-23 22:47:38 +0000 |
| commit | 362d1840c369577d369be1ee75b1cc62dfac8b43 (patch) | |
| tree | b3edd7f08ef7d29d34680905af3c0b968ac8c822 /plugins/quote | |
| parent | 14ba28e2b4ff3e93e629e4fe0842d74dd30557b3 (diff) | |
Moved a bit further the code for pattern interpretation in match goal
to anticipate support of possibly-typed patterns;
Also removed a useless nf_evar.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12606 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/quote')
0 files changed, 0 insertions, 0 deletions