Changing representation of prod over two Type: since the rule needs subtyping anyway to manage the Set and Prop cases, why not to simplify it by using subtyping also for managing Type.

1 files changed, 9 insertions, 9 deletions

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 08e962ebe2..7986648fb9 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -95,12 +95,12 @@ Formally, we call {\Sort} the set of sorts which is defined by:
 \index{Set@{\Set}}
 
 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.}%
+  %% 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
 {\Type$(i)$:\Type$(i+1)$}.
 
@@ -366,9 +366,9 @@ be derived from the following rules.
 \inference{\frac{\WTEG{T}{s}~~~~s \in\{\Prop, \Set\}~~~~~~
     \WTE{\Gamma::(x:T)}{U}{\Set}}
       { \WTEG{\forall~x:T,U}{\Set}}} 
-\inference{\frac{\WTEG{T}{\Type(i)}~~~~i\leq k~~~
-    \WTE{\Gamma::(x:T)}{U}{\Type(j)}~~~j \leq k}
-    {\WTEG{\forall~x:T,U}{\Type(k)}}}
+\inference{\frac{\WTEG{T}{\Type(i)}~~~~
+    \WTE{\Gamma::(x:T)}{U}{\Type(i)}}
+    {\WTEG{\forall~x:T,U}{\Type(i)}}}
 \item[Lam]\index{Typing rules!Lam} 
 \inference{\frac{\WTEG{\forall~x:T,U}{s}~~~~ \WTE{\Gamma::(x:T)}{t}{U}}
         {\WTEG{\lb x:T\mto t}{\forall x:T, U}}}