From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 15 Nov 2005 18:17:19 +0000 (+0000)
Subject: added content level ref
X-Git-Tag: V_0_7_2_3~70
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=22360727aa1b513bd1529ef63aadb59b92095922;p=helm.git

added content level ref
---

diff --git a/helm/papers/matita/Makefile b/helm/papers/matita/Makefile
index 07747771a..bfae83c3a 100644
--- a/helm/papers/matita/Makefile
+++ b/helm/papers/matita/Makefile
@@ -17,7 +17,7 @@ TEXS = matita.tex
 RUNS = 1
 
 # do you need bibtex?
-BIBTEX = no
+BIBTEX = yes
 
 # would you like to use pdflatex?
 PDF_VIA_PDFLATEX = yes
diff --git a/helm/papers/matita/matita.tex b/helm/papers/matita/matita.tex
index 8ed71abe6..09b1f0b79 100644
--- a/helm/papers/matita/matita.tex
+++ b/helm/papers/matita/matita.tex
@@ -283,8 +283,8 @@ depicted in Fig.~\ref{fig:inputphase}. The architecture is articulated as a
 pipline of three levels: the concrete syntax level (level 0) is the one the user
 has to deal with when inserting CIC terms; the abstract syntax level (level 2)
 is an internal representation which intuitively encodes mathematical formulae at
-the content level \NOTE{rif. per\\ content}; the formal mathematics level (level
-3) is the CIC encoding of terms.
+the content level~\cite{adams}~\cite{mkm-structure}; the formal mathematics
+level (level 3) is the CIC encoding of terms.
 
 Requirement (1) is addressed by a built-in concrete syntax for terms, described
 in Tab.~\ref{tab:termsyn}, and the extensible notation mechanisms which offers a