From 706b16c3c714f91bfff33ce340aec6f2d24fe246 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Sat, 10 Jun 2017 15:54:31 +0200
Subject: API: exports Mltop.module_is_known to both API.mli and
 grammar_API.mli

---
 API/API.mli         | 1 +
 API/grammar_API.mli | 1 +
 2 files changed, 2 insertions(+)

(limited to 'API')

diff --git a/API/API.mli b/API/API.mli
index 20a637c1fa..9714f52b91 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -3307,6 +3307,7 @@ sig
   val declare_cache_obj : (unit -> unit) -> string -> unit
   val add_known_plugin : (unit -> unit) -> string -> unit
   val add_known_module : string -> unit
+  val module_is_known : string -> bool
 end
 
 (* All items in the Proof_type module are deprecated. *)
diff --git a/API/grammar_API.mli b/API/grammar_API.mli
index 44aae771f6..4da5b380fe 100644
--- a/API/grammar_API.mli
+++ b/API/grammar_API.mli
@@ -211,6 +211,7 @@ end
 module Mltop :
 sig
   val add_known_module : string -> unit
+  val module_is_known : string -> bool
   val declare_cache_obj : (unit -> unit) -> string -> unit
 end
 module Vernacinterp :
-- 
cgit v1.2.3