diff options
Diffstat (limited to 'intf/intf.mllib')
| -rw-r--r-- | intf/intf.mllib | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/intf/intf.mllib b/intf/intf.mllib index 523e4b265..38a2a71cc 100644 --- a/intf/intf.mllib +++ b/intf/intf.mllib @@ -3,7 +3,6 @@ Evar_kinds Genredexpr Locus Notation_term -Tactypes Decl_kinds Extend Glob_term |