Fixed a problem introduced in r12607 after pattern_of_constr served

both for interpreting ltac patterns and patterns of "change pat with
term".  In particular, in the current status, Goal evars needs
mandatorily to have the hole_kind GoalEvar. If this is too complicated
to enforce, we might eventually consider another approach to the
question of interpreting patterns in general.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13428 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions