aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitignore6
-rw-r--r--Makefile3
-rw-r--r--Makefile.build65
-rw-r--r--Makefile.common15
-rw-r--r--config/Makefile.template5
-rw-r--r--dev/Makefile53
-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.pngbin6269 -> 2335 bytes
-rw-r--r--kernel/term.mli94
-rw-r--r--library/nameops.mli2
-rwxr-xr-xlibrary/nametab.mli10
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
diff --git a/Makefile b/Makefile
index f1f04e77d..ea318c111 100644
--- a/Makefile
+++ b/Makefile
@@ -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
index 06aac4597..992f2d63f 100644
--- a/ide/coq.png
+++ b/ide/coq.png
Binary files differ
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 13:36:34 +0000