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