ocamlweb

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

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

doc/intro.tex

@@ -17,9 +17,9 @@
     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}

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
 

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: 

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