diff options
author | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-29 16:33:36 +0000 |
---|---|---|
committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-29 16:33:36 +0000 |
commit | 8e66761c81648add03ed21b157a3bace716b8e08 (patch) | |
tree | 72621a076032939bc0c526c43fe57f3e674e1eca | |
parent | 28809ba4180b0421d5b0e97f9e92ba72e63bda7c (diff) |
"make source-doc" builds documentation of mli in html and pdf at
dev/ocamldoc/
old "make source-doc" that documents ml files and didn't work is now
"make ml-doc" but still don't work :-)
"make clean" cleans dev/ocamldoc/ properly
wierd? calls of dependency graph generation leave unchanged
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12978 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | .gitignore | 6 | ||||
-rw-r--r-- | Makefile | 3 | ||||
-rw-r--r-- | Makefile.build | 65 | ||||
-rw-r--r-- | Makefile.common | 15 | ||||
-rw-r--r-- | config/Makefile.template | 5 | ||||
-rw-r--r-- | dev/Makefile | 53 | ||||
-rw-r--r-- | dev/ocamldoc/docintro (renamed from dev/docintro) | 13 | ||||
-rw-r--r-- | dev/ocamldoc/html/style.css (renamed from dev/html/style.css) | 4 | ||||
-rw-r--r-- | ide/coq.png | bin | 6269 -> 2335 bytes | |||
-rw-r--r-- | kernel/term.mli | 94 | ||||
-rw-r--r-- | library/nameops.mli | 2 | ||||
-rwxr-xr-x | library/nametab.mli | 10 |
12 files changed, 127 insertions, 143 deletions
diff --git a/.gitignore b/.gitignore index 4a16b7722..f0dd91db9 100644 --- a/.gitignore +++ b/.gitignore @@ -169,3 +169,9 @@ kernel/copcodes.ml scripts/tolink.ml theories/Numbers/Natural/BigN/NMake_gen.v ide/index_urls.txt + +# mlis documentation + +dev/ocamldoc/html/ +dev/ocamldoc/coq.* +dev/ocamldoc/ocamldoc.sty @@ -227,6 +227,9 @@ voclean: devdocclean: find . -name '*.dep.ps' -o -name '*.dot' | xargs rm -f + rm -f $(OCAMLDOCDIR)/*.log $(OCAMLDOCDIR)/*.aux $(OCAMLDOCDIR)/*.toc + rm -f $(OCAMLDOCDIR)/ocamldoc.sty $(OCAMLDOCDIR)/coq.tex + rm -f $(OCAMLDOCDIR)/html/*.html ########################################################################### # Emacs tags diff --git a/Makefile.build b/Makefile.build index fe2bba29e..2dd8ec01b 100644 --- a/Makefile.build +++ b/Makefile.build @@ -584,12 +584,47 @@ install-latex: # Documentation of the source code (using ocamldoc) ########################################################################### -.PHONY: source-doc +.PHONY: source-doc mli-doc ml-doc -source-doc: - if !(test -d $(SOURCEDOCDIR)); then mkdir $(SOURCEDOCDIR); fi +source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf + +$(OCAMLDOCDIR)/coq.tex:: $(DOCMLIS:.mli=.cmi) + $(OCAMLDOC) -latex -rectypes -I /usr/lib/ocaml/camlp5 $(MLINCLUDES)\ + $(DOCMLIS) -t "Coq mlis documentation" \ + -intro $(OCAMLDOCDIR)/docintro -o $@ + +mli-doc:: $(DOCMLIS:.mli=.cmi) + $(OCAMLDOC) -html -rectypes -I /usr/lib/ocaml/camlp5 $(MLINCLUDES)\ + $(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \ + -t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \ + -css-style style.css + +%.png: %.dot + $(DOT) -Tpng $< -o $@ + +%.types.dot: %.mli + $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $< + +OCAMLDOC_MLLIBD = $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \ + `cat $| | tr ' ' '\n' | sed -n -e "/\.cmo/s/\.cmo/\.ml/p"` + +%.dot: | %.mllib.d + $(OCAMLDOC_MLLIBD) + +ml-doc: $(OCAMLDOC) -html -rectypes $(LOCALINCLUDES) -d $(SOURCEDOCDIR) $(MLSTATICFILES) +parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d + $(OCAMLDOC_MLLIBD) + +tactics/tactics.dot: | tactics/tactics.mllib.d tactics/hightactics.mllib.d + $(OCAMLDOC_MLLIBD) + +%.dot: %.mli + $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $< + +$(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex + (cd $(OCAMLDOCDIR) ; pdflatex $*.tex && pdflatex $*.tex) ########################################################################### ### Special rules @@ -657,7 +692,7 @@ ifeq ($(CHECKEDOUT),git) if test -x "`which git`"; then \ LANG=C; export LANG; \ GIT_BRANCH=$$(git branch -a | sed -ne '/^\* /s/^\* \(.*\)/\1/p'); \ - GIT_HOST=$$(hostname -f); \ + GIT_HOST=$$(hostname); \ GIT_PATH=$$(pwd); \ (echo "$${GIT_HOST}:$${GIT_PATH},$${GIT_BRANCH}") > revision.new; \ (echo "$$(git log -1 --pretty='format:%H')") >> revision.new; \ @@ -822,28 +857,6 @@ devel: $(DEBUGPRINTERS) ########################################################################### -%.types.dot: %.mli - $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $< - -%.dep.ps: %.dot - $(DOT) $(DOTOPTS) -o $@ $< - -OCAMLDOC_MLLIBD = $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \ - `cat $| | tr ' ' '\n' | sed -n -e "/\.cmo/s/\.cmo/\.ml/p"` - -%.dot: | %.mllib.d - $(OCAMLDOC_MLLIBD) - -parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d - $(OCAMLDOC_MLLIBD) - -tactics/tactics.dot: | tactics/tactics.mllib.d tactics/hightactics.mllib.d - $(OCAMLDOC_MLLIBD) - -%.dot: %.mli - $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $< - - # For emacs: # Local Variables: # mode: makefile diff --git a/Makefile.common b/Makefile.common index 4d5e00d25..9f44b3b6f 100644 --- a/Makefile.common +++ b/Makefile.common @@ -339,7 +339,20 @@ MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \ DATE=$(shell LANG=C date +"%B %Y") -SOURCEDOCDIR=dev/source-doc +########################################################################### +# Source documentation +########################################################################### + +OCAMLDOCDIR=dev/ocamldoc + +DOCMLIS=$(wildcard ./lib/*.mli ./kernel/*.mli ./library/*.mli \ + ./pretyping/*.mli ./interp/*.mli \ + ./parsing/*.mli ./proofs/*.mli \ + ./tactics/*.mli ./toplevel/*.mli) + +# Defining options to generate dependencies graphs +DOT=dot +ODOCDOTOPTS=-dot -dot-reduce # For emacs: # Local Variables: diff --git a/config/Makefile.template b/config/Makefile.template index 74ec95807..e29a4befe 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -144,11 +144,6 @@ UIMSCRIPTDIR=UIMSCRIPTPATH # Defining REVISION CHECKEDOUT=CHECKEDOUTSOURCETREE -# Defining options to generate dependencies graphs -DOT=dot -DOTOPTS=-Tps -ODOCDOTOPTS=-dot -dot-reduce - # Option to control compilation and installation of the documentation WITHDOC=WITHDOCOPT diff --git a/dev/Makefile b/dev/Makefile deleted file mode 100644 index 4693bd136..000000000 --- a/dev/Makefile +++ /dev/null @@ -1,53 +0,0 @@ -include ../config/Makefile - -LOCALINCLUDES=-I ../config -I ../tools -I ../tools/coqdoc \ - -I ../scripts -I ../lib -I ../kernel -I ../kernel/byterun -I ../library \ - -I ../proofs -I ../tactics -I ../pretyping \ - -I ../interp -I ../toplevel -I ../parsing -I ../ide/utils -I ../ide \ - -I ../plugins/omega -I ../plugins/romega \ - -I ../plugins/ring -I ../plugins/dp -I ../plugins/setoid_ring \ - -I ../plugins/xml -I ../plugins/extraction \ - -I ../plugins/fourier -I ../plugins/cc \ - -I ../plugins/funind -I ../plugins/firstorder \ - -I ../plugins/field -I ../plugins/subtac -I ../plugins/rtauto \ - -I ../plugins/recdef - -MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) - -MLIS=$(wildcard ../lib/*.mli ../kernel/*.mli ../library/*.mli \ - ../pretyping/*.mli ../interp/*.mli \ - ../parsing/*.mli ../proofs/*.mli \ - ../tactics/*.mli ../toplevel/*.mli) - -all:: html coq.pdf - -newsyntax.dvi: newsyntax.tex - latex $< - latex $< - -coq.dvi: coq.tex - latex coq - latex coq - -coq.tex:: - ocamldoc -latex -rectypes -I /usr/lib/ocaml/camlp5 $(MLINCLUDES)\ - $(MLIS) -t "Coq mlis documentation" -intro docintro -o coq.tex - -html:: - ocamldoc -html -rectypes -I /usr/lib/ocaml/camlp5 $(MLINCLUDES)\ - $(MLIS) -d html -colorize-code \ - -t "Coq mlis documentation" -intro docintro -css-style style.css - -%.dot: ../% - ocamldoc -rectypes $(MLINCLUDES) -t $* -dot -dot-reduce ../$*/*.ml ../$*/*.mli -o $@ - -%.png: %.dot - dot -Tpng $< -o $@ - -clean:: - rm -f *~ *.log *.aux - -.SUFFIXES: .tex .png - -%.pdf: %.tex - pdflatex $< && pdflatex $<
\ No newline at end of file diff --git a/dev/docintro b/dev/ocamldoc/docintro index 3d37d5374..3c0e262d4 100644 --- a/dev/docintro +++ b/dev/ocamldoc/docintro @@ -1,10 +1,9 @@ {!indexlist} -This is Coq, a proof assistant for the Calculus of Inductive Construction. +This is Coq, a proof assistant for the Calculus of Inductive Constructions. This document describes the implementation of Coq. It has been automatically generated from the source of -Coq using ocamldoc, a literate programming tool for -Objective Caml freely available at http://caml.inria.fr/. +Coq using {{:http://caml.inria.fr/}ocamldoc}. The source files are organized in several directories ordered like that: {ol {- Utility libraries : lib @@ -13,8 +12,8 @@ describes the various utility libraries used in the code of Coq.} {- Kernel : kernel -describes the \Coq\ kernel, which is a type checker for the Calculus -of Inductive Construction.} +describes the Coq kernel, which is a type checker for the Calculus +of Inductive Constructions.} {- Library : library describes the Coq library, which is made of two parts: @@ -30,11 +29,11 @@ describes the Coq library, which is made of two parts: {- Front abstract syntax of terms : interp describes the translation from Coq context-dependent -front abstract syntax of terms {v front v} to and from the +front abstract syntax of terms {v constr_expr v} to and from the context-free, untyped, raw form of constructions {v rawconstr v}.} {- Parsers and printers : parsing -describes the implementation of the \Coq\ parsers and printers.} +describes the implementation of the Coq parsers and printers.} {- Proof engine : proofs describes the Coq proof engine, which is also called diff --git a/dev/html/style.css b/dev/ocamldoc/html/style.css index b8f02a15f..c2c45b629 100644 --- a/dev/html/style.css +++ b/dev/ocamldoc/html/style.css @@ -23,11 +23,11 @@ a:active { }
.superscript {
- font-size: 4
+ font-size: 8
}
.subscript {
- font-size: 4
+ font-size: 8
}
.comment {
diff --git a/ide/coq.png b/ide/coq.png Binary files differindex 06aac4597..992f2d63f 100644 --- a/ide/coq.png +++ b/ide/coq.png diff --git a/kernel/term.mli b/kernel/term.mli index f7819d6e6..5efd95696 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -36,7 +36,8 @@ type existential_key = int type metavariable = int (** {6 Case annotation } *) -type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle (** infer printing form from number of constructor *) +type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle + | RegularStyle (** infer printing form from number of constructor *) type case_printing = { ind_nargs : int; (** length of the arity of the inductive type *) style : case_style } @@ -64,8 +65,7 @@ val eq_constr : constr -> constr -> bool type types = constr -(** {6 ... } *) -(** Functions for dealing with constr terms. +(** {5 Functions for dealing with constr terms. } The following functions are intended to simplify and to uniform the manipulation of terms. Some of these functions may be overlapped with previous ones. *) @@ -95,20 +95,21 @@ val mkType : Univ.universe -> types (** This defines the strategy to use for verifiying a Cast *) type cast_kind = VMcast | DEFAULTcast -(** Constructs the term [t1::t2], i.e. the term {% $ %}t_1{% $ %} casted with the - type {% $ %}t_2{% $ %} (that means t2 is declared as the type of t1). *) +(** Constructs the term [t1::t2], i.e. the term t{_ 1} casted with the + type t{_ 2} (that means t2 is declared as the type of t1). *) val mkCast : constr * cast_kind * constr -> constr (** Constructs the product [(x:t1)t2] *) val mkProd : name * types * types -> types val mkNamedProd : identifier -> types -> types -> types -(** non-dependant product {% $ %}t_1 \rightarrow t_2{% $ %}, an alias for - [(_:t1)t2]. Beware {% $ %}t_2{% $ %} is NOT lifted. - Eg: A |- A->A is built by [(mkArrow (mkRel 0) (mkRel 1))] *) +(** non-dependent product [t1 -> t2], an alias for + [forall (_:t1), t2]. Beware [t_2] is NOT lifted. + Eg: in context [A:Prop], [A->A] is built by [(mkArrow (mkRel 0) (mkRel 1))] +*) val mkArrow : types -> types -> constr -(** Constructs the abstraction {% $ %}[x:t_1]t_2{% $ %} *) +(** Constructs the abstraction \[x:t{_ 1}\]t{_ 2} *) val mkLambda : name * types * constr -> constr val mkNamedLambda : identifier -> types -> constr -> constr @@ -117,7 +118,7 @@ val mkLetIn : name * constr * types * constr -> constr val mkNamedLetIn : identifier -> constr -> types -> constr -> constr (** [mkApp (f,[| t_1; ...; t_n |]] constructs the application - {% $ %}(f~t_1~\dots~t_n){% $ %}. *) + {% $(f~t_1~\dots~t_n)$ %}. *) val mkApp : constr * constr array -> constr (** Constructs a constant @@ -135,12 +136,12 @@ val mkInd : inductive -> constr introduced in the section *) val mkConstruct : constructor -> constr -(** Construct the term <p>Case c of c1 | c2 .. | cn end +(** Constructs a destructor of inductive type. - [mkCase ci p c ac] stand for match [c] return [p] with [ac] presented as - describe in [ci]. + [mkCase ci p c ac] stand for match [c] as [x] in [I args] return [p] with [ac] + presented as describe in [ci]. - [p] stucture is lambda inductive_args, I inductive_args -> "return" + [p] stucture is [fun args x -> "return clause"] [ac]{^ ith} element is ith constructor case presented as {e lambda construct_args (without params). case_term } *) @@ -158,7 +159,7 @@ val mkCase : case_info * constr * constr * constr array -> constr ... with fn [ctxn] = bn.] - \noindent where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}. + where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}. *) type rec_declaration = name array * types array * constr array type fixpoint = (int array * int) * rec_declaration @@ -166,7 +167,7 @@ val mkFix : fixpoint -> constr (** If [funnames = [|f1,.....fn|]] [typarray = [|t1,...tn|]] - [bodies = [b1,.....bn]] \par\noindent + [bodies = [b1,.....bn]] then [mkCoFix (i, (funnames, typarray, bodies))] constructs the ith function of the block @@ -253,10 +254,10 @@ val is_Type : constr -> bool val iskind : constr -> bool val is_small : sorts -> bool -(** {6 ... } *) -(** Term destructors. - Destructor operations are partial functions and - raise [invalid_arg "dest*"] if the term has not the expected form. *) + +(** {6 Term destructors } *) +(** Destructor operations are partial functions and + @raise Invalid_argument "dest*" if the term has not the expected form. *) (** Destructs a DeBrujin index *) val destRel : constr -> int @@ -304,28 +305,32 @@ val destInd : constr -> inductive (** Destructs a constructor *) val destConstruct : constr -> constructor -(** Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *) +(** Destructs a [match c as x in I args return P with ... | +Ci(...yij...) => ti | ... end] (or [let (..y1i..) := c as x in I args +return P in t1], or [if c then t1 else t2]) +@return [(info,c,fun args x => P,[|...|fun yij => ti| ...|])] +where [info] is pretty-printing information *) val destCase : constr -> case_info * constr * constr * constr array (** Destructs the {% $ %}i{% $ %}th function of the block - {% $ %}{% \mathit{%}Fixpoint{% }%} ~ f_1 ~ [ctx_1] = b_1 - {% \mathit{%}with{% }%} ~ f_2 ~ [ctx_2] = b_2 - \dots - {% \mathit{%}with{% }%} ~ f_n ~ [ctx_n] = b_n{% $ %}, - where the lenght of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}. + [Fixpoint f{_ 1} ctx{_ 1} = b{_ 1} + with f{_ 2} ctx{_ 2} = b{_ 2} + ... + with f{_ n} ctx{_ n} = b{_ n}], + where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}. *) val destFix : constr -> fixpoint val destCoFix : constr -> cofixpoint -(** {6 ... } *) -(** A {e declaration} has the form (name,body,type). It is either an +(** {6 Local } *) +(** A {e declaration} has the form [(name,body,type)]. It is either an {e assumption} if [body=None] or a {e definition} if [body=Some actualbody]. It is referred by {e name} if [na] is an identifier or by {e relative index} if [na] is not an identifier (in the latter case, [na] is of type [name] but just for printing - purpose *) + purpose) *) type named_declaration = identifier * constr option * types type rel_declaration = name * constr option * types @@ -367,44 +372,47 @@ val abs_implicit : constr -> constr val lambda_implicit : constr -> constr val lambda_implicit_lift : int -> constr -> constr -(** [applist (f,args)] and co work as [mkApp] *) +(** [applist (f,args)] and its variants work as [mkApp] *) val applist : constr * constr list -> constr val applistc : constr -> constr list -> constr val appvect : constr * constr array -> constr val appvectc : constr -> constr array -> constr -(** [prodn n l b] = {% $ %}(x_1:T_1)..(x_n:T_n)b{% $ %} - where {% $ %}l = [(x_n,T_n);\dots;(x_1,T_1);Gamma]{% $ %} *) +(** [prodn n l b] = [forall (x_1:T_1)...(x_n:T_n), b] + where [l] is [(x_n,T_n)...(x_1,T_1)...]. *) val prodn : int -> (name * constr) list -> constr -> constr -(** [compose_prod l b] = {% $ %}(x_1:T_1)..(x_n:T_n)b{% $ %} - where {% $ %}l = [(x_n,T_n);\dots;(x_1,T_1)]{% $ %}. +(** [compose_prod l b] + @return [forall (x_1:T_1)...(x_n:T_n), b] + where [l] is [(x_n,T_n)...(x_1,T_1)]. Inverse of [decompose_prod]. *) val compose_prod : (name * constr) list -> constr -> constr -(** [lamn n l b] = {% $ %}[x_1:T_1]..[x_n:T_n]b{% $ %} - where {% $ %}l = [(x_n,T_n);\dots;(x_1,T_1);Gamma]{% $ %} *) +(** [lamn n l b] + @return [fun (x_1:T_1)...(x_n:T_n) => b] + where [l] is [(x_n,T_n)...(x_1,T_1)...]. *) val lamn : int -> (name * constr) list -> constr -> constr -(** [compose_lam l b] = {% $ %}[x_1:T_1]..[x_n:T_n]b{% $ %} - where {% $ %}l = [(x_n,T_n);\dots;(x_1,T_1)]{% $ %}. +(** [compose_lam l b] + @return [fun (x_1:T_1)...(x_n:T_n) => b] + where [l] is [(x_n,T_n)...(x_1,T_1)]. Inverse of [it_destLam] *) val compose_lam : (name * constr) list -> constr -> constr (** [to_lambda n l] - = {% $ %}[x_1:T_1]...[x_n:T_n]T{% $ %} - where {% $ %}l = (x_1:T_1)...(x_n:T_n)T{% $ %} *) + @return [fun (x_1:T_1)...(x_n:T_n) => T] + where [l] is [forall (x_1:T_1)...(x_n:T_n), T] *) val to_lambda : int -> constr -> constr (** [to_prod n l] - = {% $ %}(x_1:T_1)...(x_n:T_n)T{% $ %} - where {% $ %}l = [x_1:T_1]...[x_n:T_n]T{% $ %} *) + @return [forall (x_1:T_1)...(x_n:T_n), T] + where [l] is [fun (x_1:T_1)...(x_n:T_n) => T] *) val to_prod : int -> constr -> constr (** pseudo-reduction rule *) -(** [prod_appvect] {% $ %}(x1:B1;...;xn:Bn)B a1...an \rightarrow B[a1...an]{% $ %} *) +(** [prod_appvect] [forall (x1:B1;...;xn:Bn), B] [a1...an] @return [B[a1...an]] *) val prod_appvect : constr -> constr array -> constr val prod_applist : constr -> constr list -> constr diff --git a/library/nameops.mli b/library/nameops.mli index 0f1d52420..121f0ce77 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -16,7 +16,7 @@ val make_ident : string -> int option -> identifier val repr_ident : identifier -> string * int option val atompart_of_id : identifier -> string (** remove trailing digits *) -val root_of_id : identifier -> identifier (** remove trailing digits, {% $ %}'{% $ %} and {% $ %}\_{% $ %} *) +val root_of_id : identifier -> identifier (** remove trailing digits, ' and _ *) val add_suffix : identifier -> string -> identifier val add_prefix : string -> identifier -> identifier diff --git a/library/nametab.mli b/library/nametab.mli index 4303d86a3..aaef53e4a 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -53,6 +53,7 @@ open Libnames The [user_name] can be for example the shortest non ambiguous [qualid] or the [full_user_name] or [identifier]. Such a function can also have a local context argument.}} + *) @@ -67,12 +68,11 @@ val error_global_constant_not_found_loc : loc -> qualid -> 'a (** {6 Register visibility of things } *) (** The visibility can be registered either - - for all suffixes not shorter then a given int -- when the - object is loaded inside a module -- or - + object is loaded inside a module -- or - for a precise suffix, when the module containing (the module containing ...) the object is opened (imported) + *) type visibility = Until of int | Exactly of int @@ -133,8 +133,8 @@ val full_name_cci : qualid -> full_path val full_name_modtype : qualid -> full_path val full_name_module : qualid -> dir_path -(** {6 ... } *) -(** Reverse lookup -- finding user names corresponding to the given +(** {6 Reverse lookup } + Finding user names corresponding to the given internal name *) (** Returns the full path bound to a global reference or syntactic |