From 47f6154a7647f44411c41deb6b42642d281a9296 Mon Sep 17 00:00:00 2001
From: Anton Trunov
Date: Thu, 15 Nov 2018 11:27:52 +0100
Subject: Add a section on documenting code

Based on the discussion here:
https://github.com/math-comp/math-comp/pull/242
---
 CONTRIBUTING.md | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 96c3b76..467baff 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -129,3 +129,20 @@ Abbreviations are in the header of the file which introduce them. We list here t
   - `z` -- an int argument
 #### Typical search pattern
 `Search _ "prefix" "suffix"* (symbol|pattern)* in library.`
+
+## Doc style.
+### Header documentary comments
+We try to document types, definitions and notations precisely, but only describe
+the lemmas and theorems in general terms, because we don't want to discourage users
+from actually reading the documentation.
+There are some exceptions for some particularly important theorems.
+
+### Commenting source code
+The MathComp library uses exclusively block comments, with 80-character lines
+enclosed in the `(*` / `*)` delimiters, e.g.
+```
+(* Lorem ipsum dolor sit amet, consectetuer adipiscing elit.  Donec hendrerit *)
+(* tempor tellus.  Donec pretium posuere tellus.  Proin quam nisl, tincidunt  *)
+(* et, mattis eget, convallis nec, purus.                                     *)
+```
+Multiline comments are strictly limited to out-commented code.
-- 
cgit v1.2.3