diff options
| author | Vincent Laporte | 2018-03-06 20:29:06 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-03-07 17:31:47 +0000 |
| commit | 33bf4f2c5c60114eb6db4a8e082ff8882923f6c8 (patch) | |
| tree | a07c626739bf195b5d7a938c5fe4ee5594c2c1a1 /pretyping/typeclasses_errors.ml | |
| parent | 66c523bcac8b64e202baa084bf24f5b57c61fcd6 (diff) | |
[vernac] Warn when using “Require” in a section
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions