diff options
Diffstat (limited to 'interp/interp.mllib')
| -rw-r--r-- | interp/interp.mllib | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/interp/interp.mllib b/interp/interp.mllib index 234487bc9..991cfac57 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -4,7 +4,8 @@ Ppextend Notation Dumpglob Genarg -Syntax_def +Syntax_def +Smartlocate Reserve Impargs Implicit_quantifiers |