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 /parsing/pptactic.ml | |
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 'parsing/pptactic.ml')
0 files changed, 0 insertions, 0 deletions