ocamlweb

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@163 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 21 insertions, 6 deletions

diff --git a/Makefile b/Makefile
index 5fb8f9ff2a..64bec2282a 100644
--- a/Makefile
+++ b/Makefile
@@ -129,12 +129,13 @@ doc: doc/coq.tex
 LPLIB = lib/doc.tex $(LIB:.cmo=.mli)
 LPKERNEL = kernel/doc.tex $(KERNEL:.cmo=.mli)
 LPLIBRARY = library/doc.tex $(LIBRARY:.cmo=.mli)
+LPPRETYPING = pretyping/doc.tex pretyping/rawterm.mli $(PRETYPING:.cmo=.mli)
+LPPARSING =$(PARSING:.cmo=.mli)
 LPPROOFS = proofs/doc.tex $(PROOFS:.cmo=.mli)
 LPTACTICS = tactics/doc.tex $(TACTICS:.cmo=.mli)
-LPPRETYPING = pretyping/rawterm.mli $(PRETYPING:.cmo=.mli)
 LPTOPLEVEL = toplevel/doc.tex $(TOPLEVEL:.cmo=.mli)
 LPFILES = doc/macros.tex doc/intro.tex $(LPLIB) $(LPKERNEL) $(LPLIBRARY) \
-	  $(LPPROOFS) $(LPTACTICS) $(LPPRETYPING) $(LPTOPLEVEL)
+	  $(LPPRETYPING) $(LPPROOFS) $(LPTACTICS) $(LPTOPLEVEL)
 
 doc/coq.tex: doc/preamble.tex $(LPFILES)
 	cat doc/preamble.tex > doc/coq.tex
diff --git a/doc/intro.tex b/doc/intro.tex
index 6a34ca48bb..4cec8673f4 100644
--- a/doc/intro.tex
+++ b/doc/intro.tex
@@ -17,9 +17,9 @@ described here as separate chapters.
     Utility libraries \dotfill & \refsec{lib}     & \pageref{lib}     \\[0.5em]
     Kernel            \dotfill & \refsec{kernel}  & \pageref{kernel}  \\[0.5em]
     Library           \dotfill & \refsec{library} & \pageref{library} \\[0.5em]
+    Pretyping     \dotfill & \refsec{pretyping} & \pageref{pretyping} \\[0.5em]
     Proof engine      \dotfill & \refsec{proofs}  & \pageref{proofs}  \\[0.5em]
     Tactics           \dotfill & \refsec{tactics} & \pageref{tactics} \\[0.5em]
-    \dots & & \\[0.5em]
     Toplevel          \dotfill & \refsec{toplevel}& \pageref{toplevel}\\[0.5em]
   \end{tabular}
 \end{center}
\ No newline at end of file
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 9945b36cb7..a5244b6804 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -181,8 +181,8 @@ val whd_meta : (int * constr) list -> constr -> constr
 val plain_instance : (int * constr) list -> constr -> constr
 val instance : (int * constr) list -> 'a reduction_function
 
-(* whd_ise raise Uninstantiated_evar if an evar remains uninstantiated *)
-(* the '*_ise1*' leave uninstantiated evar as it *)
+(* [whd_ise] raise [Uninstantiated_evar] if an evar remains uninstantiated *)
+(* the *[_ise1]* leave uninstantiated evar as it *)
 
 exception Uninstantiated_evar of int
 
diff --git a/pretyping/doc.tex b/pretyping/doc.tex
new file mode 100644
index 0000000000..d92a027eaf
--- /dev/null
+++ b/pretyping/doc.tex
@@ -0,0 +1,14 @@
+
+\newpage
+\section*{Pre-typing}
+
+\ocwsection \label{pretyping}
+
+\bigskip
+\begin{center}\epsfig{file=pretyping.dep.ps,width=\linewidth}\end{center}
+
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: t
+%%% End: 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 5dabb016fc..b4fee1cd29 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -45,7 +45,7 @@ val ise_resolve : bool -> 'c evar_map -> (int * constr) list ->
 val ise_resolve_type : bool -> 'c evar_map -> (int * constr) list ->
   unsafe_env -> rawconstr -> typed_type
 
-(* Call ise_resolve with empty metamap and fail_evar=true. The boolean says
+(* Call [ise_resolve] with empty metamap and [fail_evar=true]. The boolean says
  * if we must coerce to a type *)
 val ise_resolve1 : bool -> 'c evar_map -> unsafe_env -> rawconstr -> constr