From 5330263aaccb3ba9e7fcb8fada0737491fd99645 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 23 Oct 2015 17:51:06 +0200
Subject: Removing note on shifting the hierarchy by 1 in 8.4, which makes
 things more complicated than needed.

---
 doc/refman/RefMan-cic.tex | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 5002b905c7..08e962ebe2 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -94,13 +94,14 @@ Formally, we call {\Sort} the set of sorts which is defined by:
 \index{Prop@{\Prop}}
 \index{Set@{\Set}}
 
-The sorts enjoy the following properties\footnote{In the Reference
+The sorts enjoy the following properties%\footnote{In the Reference
   Manual of versions of {\Coq} prior to 8.4, the level of {\Type} typing
   {\Prop} and {\Set} was numbered $0$. From {\Coq} 8.4, it started to be
   numbered $1$ so as to be able to leave room for re-interpreting
   {\Set} in the hierarchy as {\Type$(0)$}. This change also put the
   reference manual in accordance with the internal conventions adopted
-  in the implementation.}: {\Prop:\Type$(1)$}, {\Set:\Type$(1)$} and
+  in the implementation.}%
+: {\Prop:\Type$(1)$}, {\Set:\Type$(1)$} and
 {\Type$(i)$:\Type$(i+1)$}.
 
 The user does not have to mention explicitly the index $i$ when referring to
-- 
cgit v1.2.3