Fixed a hole in glob_tactic that allowed some Ltac code to refer to

statically unbound variables (revealed by an assert failure in
Tacinterp.subst_rawconstr_and_expr). In particular, tauto's use of
name "id" was bypassing the globalization phase (apparently in an safe
way though).

Added a new kind of anomaly usable in case an anomaly results of an
unexpected exception.



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

0 files changed, 0 insertions, 0 deletions