From 5824a2c9362a6e33eb43b5e0e2c7572abeee2511 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 16:41:58 +0100 Subject: CLEANUP: removing unnecessary alias --- intf/vernacexpr.mli | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'intf/vernacexpr.mli') 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 -- cgit v1.2.3