aboutsummaryrefslogtreecommitdiffstats
path: root/src/common
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2022-03-26 15:48:47 +0000
committerYann Herklotz <git@yannherklotz.com>2022-03-26 15:48:47 +0000
commitdd8d4ae9c320668ac5fd70f72ea76b768edf8165 (patch)
treea7c6fa3f15ab227516b00b8186789aeb420b642e /src/common
parent30baa719fb15c45b13cb869056e51ec7446c0207 (diff)
downloadvericert-dd8d4ae9c320668ac5fd70f72ea76b768edf8165.tar.gz
vericert-dd8d4ae9c320668ac5fd70f72ea76b768edf8165.zip
Remove literal files again
Diffstat (limited to 'src/common')
-rw-r--r--src/common/Maps.v5
1 files changed, 3 insertions, 2 deletions
diff --git a/src/common/Maps.v b/src/common/Maps.v
index 13ca276..cb9dc2c 100644
--- a/src/common/Maps.v
+++ b/src/common/Maps.v
@@ -29,8 +29,9 @@ Import PTree.
Local Open Scope error_monad_scope.
-(** Instance of traverse for [PTree] and [Errors]. This should maybe be generalised
- in the future. *)
+(*|
+Instance of traverse for ``PTree`` and ``Errors``. This should maybe be generalised in the future.
+|*)
Module PTree.