From f73d7c4614d000f068550b5144d80b7eceed58e9 Mon Sep 17 00:00:00 2001
From: pboutill
Date: Thu, 29 Apr 2010 09:56:37 +0000
Subject: Move from ocamlweb to ocamdoc to generate mli documentation

dev/ocamlweb-doc has been erased. I hope no one still use the
"new-parse" it generate.

In dev/,
make html will generate in dev/html/ "clickable version of mlis". (as
the caml standard library)
make coq.pdf will generate nearly the same awfull stuff that coq.ps was.
make {kernel,lib,parsing,..}.{dot,png} will do the dependancy graph of
the given directory.

ocamldoc comment syntax is here :
http://caml.inria.fr/pub/docs/manual-ocaml/manual029.html

The possibility to put graphs in pdf/html seems to be lost.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12969 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/pretype_errors.mli | 36 +++++++++++++++++-------------------
 1 file changed, 17 insertions(+), 19 deletions(-)

(limited to 'pretyping/pretype_errors.mli')

diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index ca48f70211..9b6216a126 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -1,14 +1,13 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
+(***********************************************************************
+    v      *   The Coq Proof Assistant  /  The Coq Development Team     
+   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
+     \VV/  *************************************************************
+      //   *      This file is distributed under the terms of the       
+           *       GNU Lesser General Public License Version 2.1        
+  ***********************************************************************)
 
 (*i $Id$ i*)
 
-(*i*)
 open Pp
 open Util
 open Names
@@ -17,14 +16,13 @@ open Sign
 open Environ
 open Rawterm
 open Inductiveops
-(*i*)
 
-(*s The type of errors raised by the pretyper *)
+(** {6 The type of errors raised by the pretyper } *)
 
 type pretype_error =
-  (* Old Case *)
+  (** Old Case *)
   | CantFindCaseType of constr
-  (* Unification *)
+  (** Unification *)
   | OccurCheck of existential_key * constr
   | NotClean of existential_key * constr * Evd.hole_kind
   | UnsolvableImplicit of Evd.evar_info * Evd.hole_kind *
@@ -35,7 +33,7 @@ type pretype_error =
   | CannotGeneralize of constr
   | NoOccurrenceFound of constr * identifier option
   | CannotFindWellTypedAbstraction of constr * constr list
-  (* Pretyping *)
+  (** Pretyping *)
   | VarNotFound of identifier
   | UnexpectedType of constr * constr
   | NotProduct of constr
@@ -44,7 +42,7 @@ exception PretypeError of env * pretype_error
 
 val precatchable_exception : exn -> bool
 
-(* Presenting terms without solved evars *)
+(** Presenting terms without solved evars *)
 val nf_evar :  Evd.evar_map -> constr -> constr
 val j_nf_evar :  Evd.evar_map -> unsafe_judgment -> unsafe_judgment
 val jl_nf_evar :
@@ -55,7 +53,7 @@ val tj_nf_evar :
    Evd.evar_map -> unsafe_type_judgment -> unsafe_type_judgment
 
 
-(* Raising errors *)
+(** Raising errors *)
 val error_actual_type_loc :
   loc -> env ->  Evd.evar_map -> unsafe_judgment -> constr -> 'b
 
@@ -87,7 +85,7 @@ val error_not_a_type_loc :
 
 val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b
 
-(*s Implicit arguments synthesis errors *)
+(** {6 Implicit arguments synthesis errors } *)
 
 val error_occur_check : env ->  Evd.evar_map -> existential_key -> constr -> 'b
 
@@ -105,12 +103,12 @@ val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr -
 val error_cannot_find_well_typed_abstraction : env -> Evd.evar_map ->
       constr -> constr list -> 'b
 
-(*s Ml Case errors *)
+(** {6 Ml Case errors } *)
 
 val error_cant_find_case_type_loc :
   loc -> env ->  Evd.evar_map -> constr -> 'b
 
-(*s Pretyping errors *)
+(** {6 Pretyping errors } *)
 
 val error_unexpected_type_loc :
   loc -> env ->  Evd.evar_map -> constr -> constr -> 'b
@@ -118,6 +116,6 @@ val error_unexpected_type_loc :
 val error_not_product_loc :
   loc -> env ->  Evd.evar_map -> constr -> 'b
 
-(*s Error in conversion from AST to rawterms *)
+(** {6 Error in conversion from AST to rawterms } *)
 
 val error_var_not_found_loc : loc -> identifier -> 'b
-- 
cgit v1.2.3