diff options
Diffstat (limited to 'intf/intf.mllib')
| -rw-r--r-- | intf/intf.mllib | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/intf/intf.mllib b/intf/intf.mllib deleted file mode 100644 index 2b8960d3..00000000 --- a/intf/intf.mllib +++ /dev/null @@ -1,11 +0,0 @@ -Constrexpr -Evar_kinds -Genredexpr -Locus -Extend -Notation_term -Decl_kinds -Glob_term -Misctypes -Pattern -Vernacexpr |