diff options
Diffstat (limited to 'intf/intf.mllib')
| -rw-r--r-- | intf/intf.mllib | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/intf.mllib b/intf/intf.mllib index 38a2a71cc..2b8960d3f 100644 --- a/intf/intf.mllib +++ b/intf/intf.mllib @@ -2,9 +2,9 @@ Constrexpr Evar_kinds Genredexpr Locus +Extend Notation_term Decl_kinds -Extend Glob_term Misctypes Pattern |