Merge pull request #26 from Villetaneuse/tryToFixRequireImport

try to fix coqdoc emphasis
coq · Jun 22, 2024 · ad6dab8 · ad6dab8
2 parents f7f3c3a + 0fcbe5d
commit ad6dab8
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/RequireImportTutorial.v b/src/RequireImportTutorial.v
@@ -266,7 +266,7 @@ Qed.
 (** This dot syntax is reminiscent of what we used for library files, and it is
     no accident. In fact,
 
-    _library files are modules._
+    _library files are modules_.
 
     This is the most important fact to take home from this tutorial, and the
     main reason to study a part of Coq's module system.