Fixing the "capture" check newly introduced in r15122 when

internalizing declaration of contexts of the form "(x y : P x)":
- don't forget to catch the error in intern_context;
- check capture on glob_constr rather than constr_expr so that binders
  possibly introduced by notations are recognized as such;
- give a more expressive error message.

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

0 files changed, 0 insertions, 0 deletions