From 184357ec267dcf5922aedd7eabd56cf29ea4341f Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 5 Sep 2018 11:44:11 +0200
Subject: [doc] nodes in ssr are monospace

---
 plugins/ssr/ssrbool.v   | 2 ++
 plugins/ssr/ssreflect.v | 2 ++
 plugins/ssr/ssrfun.v    | 2 ++
 3 files changed, 6 insertions(+)

(limited to 'plugins')

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.
 
diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index 80e9cc8489..01af67912a 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.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 Import Bool. (* For bool_scope delimiter 'bool'. *)
 Require Import ssrmatching.
 Declare ML Module "ssreflect_plugin".
diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v
index 4d458ee765..e2c0ed7c8b 100644
--- a/plugins/ssr/ssrfun.v
+++ b/plugins/ssr/ssrfun.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 Import ssreflect.
 
 
-- 
cgit v1.2.3