From 615290d0f9d5cad7c508d45cf4ab89aecff033b2 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 1 Jun 2018 02:37:15 +0200 Subject: [api] Remove Misctypes. We move the last 3 types to more adequate places. --- vernac/vernacentries.mli | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'vernac/vernacentries.mli') diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index f6199e820..3c88a3443 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -8,9 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Misctypes - -val dump_global : Libnames.reference or_by_notation -> unit +val dump_global : Libnames.reference Constrexpr.or_by_notation -> unit (** Vernacular entries *) val vernac_require : -- cgit v1.2.3