diff options
| author | herbelin | 2013-06-02 21:31:26 +0000 |
|---|---|---|
| committer | herbelin | 2013-06-02 21:31:26 +0000 |
| commit | 164b3bdb69f60b9bbbe83abce73c6256869d1f4b (patch) | |
| tree | b66508896a009c951fc5b83f4a40f027eccaa892 /plugins | |
| parent | 1b2a6326876c67bf25657ecd7c0765cacd1cde75 (diff) | |
Modest protection against "injection" and co raising anomaly in
-nois mode. This is not perfect yet. E.g. "injection" used while
before eq is defined while compiling Logic.v would raise an anomaly.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16548 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions