diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-11 20:10:28 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-11 20:10:28 +0000 |
| commit | 8cce186d907eb1774469e06dba44d6204d66e80a (patch) | |
| tree | 6911cc05389f9adce2b4db9e26049cc360f9d52d /LICENSE | |
| parent | b1057e9eb29e8a5df185c42c9a7114e8d4496e91 (diff) | |
Safe_typing: adding a inductive block adds many labels (fix #2603)
When adding an inductive block in the environment, we now check that
no types or constructors in this block correspond to a label already
used in the current module. The earlier check was to try only the
first inductive type (which serves as label in the structure_body),
that was causing awkward situations, cf. for instance #2603.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14553 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'LICENSE')
0 files changed, 0 insertions, 0 deletions