From 5a5f774de94a1e822d5f8b079178dcef7ffdd0b0 Mon Sep 17 00:00:00 2001 From: pboutill Date: Mon, 3 May 2010 16:57:18 +0000 Subject: 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 --- Makefile.build | 4 ++-- dev/db | 4 ---- ide/coq.png | Bin 2335 -> 6269 bytes pretyping/rawterm.mli | 63 +++++++++++++++++++++++--------------------------- 4 files changed, 31 insertions(+), 40 deletions(-) diff --git a/Makefile.build b/Makefile.build index 6b11353b96..9b6452658c 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 82ec9f6ea9..77dc3eb60a 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 992f2d63f5..06aac45977 100644 Binary files a/ide/coq.png and b/ide/coq.png differ diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 9e2d1f28cf..0c8f154726 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -1,37 +1,34 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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 } -- cgit v1.2.3