Rename \Tree to \NatTree

1 files changed, 14 insertions, 14 deletions

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 542fdf51e..2695c5eee 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -883,8 +883,8 @@ the type $V$ satisfies the nested positivity condition for $X$
 \settowidth\framecharacterwidth{\hh}
 \newcommand\ws{\hbox{}\hskip\the\framecharacterwidth}
 \newcommand\ruleref[1]{\hskip.25em\dots\hskip.2em{\em (bullet #1)}}
-\newcommand{\Tree}{\mbox{\textsf{nattree}}}
-\newcommand{\TreeA}{\mbox{\textsf{nattree}}~\ensuremath{A}}
+\newcommand{\NatTree}{\mbox{\textsf{nattree}}}
+\newcommand{\NatTreeA}{\mbox{\textsf{nattree}}~\ensuremath{A}}
 \newcommand{\cnode}{\mbox{\textsf{node}}}
 \newcommand{\cleaf}{\mbox{\textsf{leaf}}}
 
@@ -897,25 +897,25 @@ Inductive nattree (A:Type) : Type :=
 \end{verbatim}
 
 \begin{latexonly}
-\noindent Then every instantiated constructor of $\TreeA$ satisfies the nested positivity condition for $\Tree$\\
+\noindent Then every instantiated constructor of $\NatTreeA$ satisfies the nested positivity condition for $\NatTree$\\
 \noindent
 \ws\ws\vv\\
-\ws\ws\vh\hh\ws concerning type $\TreeA$ of constructor $\cleaf$:\\
-\ws\ws\vv\ws\ws\ws\ws Type $\TreeA$ of constructor $\cleaf$ satisfies the positivity condition for $\Tree$\\
-\ws\ws\vv\ws\ws\ws\ws because $\Tree$ does not appear in any (real) arguments of the type of that constructor\\
-\ws\ws\vv\ws\ws\ws\ws (primarily because $\Tree$ does not have any (real) arguments)\ruleref1\\
+\ws\ws\vh\hh\ws concerning type $\NatTreeA$ of constructor $\cleaf$:\\
+\ws\ws\vv\ws\ws\ws\ws Type $\NatTreeA$ of constructor $\cleaf$ satisfies the positivity condition for $\NatTree$\\
+\ws\ws\vv\ws\ws\ws\ws because $\NatTree$ does not appear in any (real) arguments of the type of that constructor\\
+\ws\ws\vv\ws\ws\ws\ws (primarily because $\NatTree$ does not have any (real) arguments)\ruleref1\\
 \ws\ws\vv\\
-\ws\ws\hv\hh\ws concerning type $\forall~A\ra(\NN\ra\TreeA)\ra\TreeA$ of constructor $\cnode$:\\
-    \ws\ws\ws\ws\ws\ws\ws Type $\forall~A:\Type,A\ra(\NN\ra\TreeA)\ra\TreeA$ of constructor $\cnode$\\
-\ws\ws\ws\ws\ws\ws\ws satisfies the positivity condition for $\Tree$ because:\\
+\ws\ws\hv\hh\ws concerning type $\forall~A\ra(\NN\ra\NatTreeA)\ra\NatTreeA$ of constructor $\cnode$:\\
+    \ws\ws\ws\ws\ws\ws\ws Type $\forall~A:\Type,A\ra(\NN\ra\NatTreeA)\ra\NatTreeA$ of constructor $\cnode$\\
+\ws\ws\ws\ws\ws\ws\ws satisfies the positivity condition for $\NatTree$ because:\\
 \ws\ws\ws\ws\ws\ws\ws\vv\\
-\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\Tree$ occurs only strictly positively in $\Type$\ruleref1\\
+\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\NatTree$ occurs only strictly positively in $\Type$\ruleref1\\
 \ws\ws\ws\ws\ws\ws\ws\vv\\
-\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\Tree$ occurs only strictly positively in $A$\ruleref1\\
+\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\NatTree$ occurs only strictly positively in $A$\ruleref1\\
 \ws\ws\ws\ws\ws\ws\ws\vv\\
-    \ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\Tree$ occurs only strictly positively in $\NN\ra\TreeA$\ruleref{3+2}\\
+    \ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\NatTree$ occurs only strictly positively in $\NN\ra\NatTreeA$\ruleref{3+2}\\
 \ws\ws\ws\ws\ws\ws\ws\vv\\
-\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $\Tree$ satisfies the positivity condition for $\TreeA$\ruleref1
+\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $\NatTree$ satisfies the positivity condition for $\NatTreeA$\ruleref1
 \end{latexonly}
 \begin{rawhtml}
 <pre>