aboutsummaryrefslogtreecommitdiff
path: root/library/libnames.mli
diff options
context:
space:
mode:
Diffstat (limited to 'library/libnames.mli')
-rw-r--r--library/libnames.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/library/libnames.mli b/library/libnames.mli
index 9960603cbb..bbb4d2a058 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -94,8 +94,8 @@ val qualid_basename : qualid -> Id.t
val default_library : DirPath.t
(** This is the root of the standard library of Coq *)
-val coq_root : module_ident (** "Coq" *)
-val coq_string : string (** "Coq" *)
+val coq_root : module_ident (* "Coq" *)
+val coq_string : string (* "Coq" *)
(** This is the default root prefix for developments which doesn't
mention a root *)