aboutsummaryrefslogtreecommitdiff
path: root/vernac/mltop.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/mltop.mli')
-rw-r--r--vernac/mltop.mli3
1 files changed, 0 insertions, 3 deletions
diff --git a/vernac/mltop.mli b/vernac/mltop.mli
index ed1f9a12d8..3d796aa4aa 100644
--- a/vernac/mltop.mli
+++ b/vernac/mltop.mli
@@ -21,9 +21,6 @@ type toplevel = {
(** Sets and initializes a toplevel (if any) *)
val set_top : toplevel -> unit
-(** Are we in a native version of Coq? *)
-val is_native : bool
-
(** Removes the toplevel (if any) *)
val remove : unit -> unit