ocamldoc related fixes

 - coq logo isn't destructed anymore

 - Erase debug printers not implemented for new proofs

 - ocamldoc compatible comments for pretyping/rawterm.mli

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

4 files changed, 31 insertions, 40 deletions

diff --git a/Makefile.build b/Makefile.build
index 6b11353b9..9b6452658 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -601,10 +601,10 @@ mli-doc:: $(DOCMLIS:.mli=.cmi)
 	-t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \
 	-css-style style.css
 
-%.png: %.dot
+%_dep.png: %.dot
 	$(DOT) -Tpng $< -o $@
 
-%.types.dot: %.mli
+%_types.dot: %.mli
 	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $< 
 
 OCAMLDOC_MLLIBD = $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \
diff --git a/dev/db b/dev/db
index 82ec9f6ea..77dc3eb60 100644
--- a/dev/db
+++ b/dev/db
@@ -28,12 +28,8 @@ install_printer Top_printers.pptype
 install_printer Top_printers.ppj
 install_printer Top_printers.ppenv
 
-install_printer Top_printers.ppgoal
-install_printer Top_printers.ppsigmagoal
-install_printer Top_printers.pproof
 install_printer Top_printers.ppmetas
 install_printer Top_printers.ppevm
-install_printer Top_printers.ppclenv
 
 install_printer Top_printers.pptac
 install_printer Top_printers.ppobj
diff --git a/ide/coq.png b/ide/coq.png
index 992f2d63f..06aac4597 100644
--- a/ide/coq.png
+++ b/ide/coq.png
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 9e2d1f28c..0c8f15472 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -1,37 +1,34 @@
-(************************************************************************)
-(*  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*)
+(***********************************************************************
+    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        
+  ***********************************************************************)
+
+(**Untyped intermediate terms, after constr_expr and before constr
+
+   Resolution of names, insertion of implicit arguments placeholder,
+   and notations are done, but coercions, inference of implicit
+   arguments and pattern-matching compilation are not. *)
+
 open Util
 open Names
 open Sign
 open Term
 open Libnames
 open Nametab
-(*i*)
 
-(**********************************************************************)
-(* The kind of patterns that occurs in "match ... with ... end"       *)
+(**  The kind of patterns that occurs in "match ... with ... end"
 
-(* locs here refers to the ident's location, not whole pat *)
-(* the last argument of PatCstr is a possible alias ident for the pattern *)
+     locs here refers to the ident's location, not whole pat the last
+     argument of PatCstr is a possible alias ident for the pattern *)
 type cases_pattern =
   | PatVar of loc * name
   | PatCstr of loc * constructor * cases_pattern list * name
 
 val cases_pattern_loc : cases_pattern -> loc
 
-(**********************************************************************)
-(* Untyped intermediate terms, after constr_expr and before constr    *)
-(* Resolution of names, insertion of implicit arguments placeholder,  *)
-(* and notations are done, but coercions, inference of implicit       *)
-(* arguments and pattern-matching compilation are not                 *)
-
 type patvar = identifier
 
 type rawsort = RProp of Term.contents | RType of Univ.universe option
@@ -53,13 +50,13 @@ type 'a with_bindings = 'a * 'a bindings
 
 type 'a cast_type =
   | CastConv of cast_kind * 'a
-  | CastCoerce (* Cast to a base type (eg, an underlying inductive type) *)
+  | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *)
 
 type rawconstr =
   | RRef of (loc * global_reference)
   | RVar of (loc * identifier)
   | REvar of loc * existential_key * rawconstr list option
-  | RPatVar of loc * (bool * patvar) (* Used for patterns only *)
+  | RPatVar of loc * (bool * patvar) (** Used for patterns only *)
   | RApp of loc * rawconstr * rawconstr list
   | RLambda of loc * name * binding_kind *  rawconstr * rawconstr
   | RProd of loc * name * binding_kind * rawconstr * rawconstr
@@ -96,7 +93,7 @@ and cases_clauses = cases_clause list
 
 val cases_predicate_names : tomatch_tuples -> name list
 
-(*i - if PRec (_, names, arities, bodies) is in env then arities are
+(* - if PRec (_, names, arities, bodies) is in env then arities are
    typed in env too and bodies are typed in env enriched by the
    arities incrementally lifted
 
@@ -105,38 +102,36 @@ val cases_predicate_names : tomatch_tuples -> name list
 
    - boolean in POldCase means it is recursive
    - option in PHole tell if the "?" was apparent or has been implicitely added
-i*)
+*)
 
 val map_rawconstr : (rawconstr -> rawconstr) -> rawconstr -> rawconstr
 
-(*i
+(*
 val map_rawconstr_with_binders_loc : loc ->
   (identifier -> 'a -> identifier * 'a) ->
   ('a -> rawconstr -> rawconstr) -> 'a -> rawconstr -> rawconstr
-i*)
+*)
 
 val occur_rawconstr : identifier -> rawconstr -> bool
 val free_rawvars : rawconstr -> identifier list
 val loc_of_rawconstr : rawconstr -> loc
 
-(**********************************************************************)
-(* Conversion from rawconstr to cases pattern, if possible            *)
-
-(* Take the current alias as parameter, raise Not_found if *)
-(* translation is impossible *)
+(** Conversion from rawconstr to cases pattern, if possible
+    
+    Take the current alias as parameter, 
+    @raise Not_found if translation is impossible *)
 
 val cases_pattern_of_rawconstr : name -> rawconstr -> cases_pattern
 
 val rawconstr_of_closed_cases_pattern : cases_pattern -> name * rawconstr
 
-(**********************************************************************)
-(* Reduction expressions                                              *)
+(** {6 Reduction expressions} *)
 
 type 'a raw_red_flag = {
   rBeta : bool;
   rIota : bool;
   rZeta : bool;
-  rDelta : bool; (* true = delta all but rConst; false = delta only on rConst*)
+  rDelta : bool; (** true = delta all but rConst; false = delta only on rConst*)
   rConst : 'a list
 }