diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-16 16:41:58 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-18 15:58:47 +0100 |
| commit | 5824a2c9362a6e33eb43b5e0e2c7572abeee2511 (patch) | |
| tree | 4ca1918717c59fb9bf1f6e16d22172dccf5b3030 /intf/vernacexpr.mli | |
| parent | 20641795624dbb03da0401e4dc503660e5e73df6 (diff) | |
CLEANUP: removing unnecessary alias
Diffstat (limited to 'intf/vernacexpr.mli')
| -rw-r--r-- | intf/vernacexpr.mli | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 07a206b53..4bc3a9e60 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -19,7 +19,6 @@ open Libnames type lident = Id.t located type lname = Name.t located type lstring = string located -type lreference = reference type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation @@ -330,8 +329,8 @@ type vernac_expr = | VernacBeginSection of lident | VernacEndSegment of lident | VernacRequire of - lreference option * export_flag option * lreference list - | VernacImport of export_flag * lreference list + reference option * export_flag option * reference list + | VernacImport of export_flag * reference list | VernacCanonical of reference or_by_notation | VernacCoercion of obsolete_locality * reference or_by_notation * class_rawexpr * class_rawexpr |