From 2b97a257956d307e7cb9ad7d4920fb5db969b69b Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Thu, 22 Oct 2020 12:06:31 +0200
Subject: Update CONTRIBUTING.md

---
 CONTRIBUTING.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 19ab0e5..26baba2 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -116,6 +116,7 @@ Abbreviations are in the header of the file which introduces them. We list here
   - `b` -- a boolean argument, as in `andbb : idempotent andb.`
   - `C` -- commutativity, as in `andbC : commutative andb.`
         -- alternatively, predicate or set complement, as in `predC.`
+        -- alternatively, constant.
   - `CA` -- left commutativity.
   - `D` -- predicate or set difference, as in `predD.`
   - `E` -- elimination lemma, as in `negbFE : ~~ b = false -> b.`
-- 
cgit v1.2.3