aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr/ssrbool.v
diff options
context:
space:
mode:
authorEnrico Tassi2018-09-05 11:44:11 +0200
committerEnrico Tassi2018-11-07 12:23:06 +0100
commit184357ec267dcf5922aedd7eabd56cf29ea4341f (patch)
tree6c7698baf1c68d56a17c8fd53a00f577f4f68d42 /plugins/ssr/ssrbool.v
parentfefe909fb84964efadf6d158379deea6e07ada73 (diff)
[doc] nodes in ssr are monospace
Diffstat (limited to 'plugins/ssr/ssrbool.v')
-rw-r--r--plugins/ssr/ssrbool.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v
index cf4b8c1ce9..a618fc781f 100644
--- a/plugins/ssr/ssrbool.v
+++ b/plugins/ssr/ssrbool.v
@@ -10,6 +10,8 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(** #<style> .doc { font-family: monospace; white-space: pre; } </style># **)
+
Require Bool.
Require Import ssreflect ssrfun.