coq/doc/stdlib/make-library-index, branch master

Fix #11749: don't warn for hidden files.

2020-03-04T15:26:29+00:00

[build] Consolidate stdlib's .v files under a single directory.

2020-02-13T20:12:03+00:00

Currently, `.v` under the `Coq.` prefix are found in both `theories`
and `plugins`. Usually these two directories are merged by special
loadpath code that allows double-binding of the prefix.

This adds some complexity to the build and loadpath system; and in
particular, it prevents from handling the `Coq.*` prefix in the
simple, `-R theories Coq` standard way.

We thus move all `.v` files to theories, leaving `plugins` as an
OCaml-only directory, and modify accordingly the loadpath / build
infrastructure.

Note that in general `plugins/foo/Foo.v` was not self-contained, in
the sense that it depended on files in `theories` and files in
`theories` depended on it; moreover, Coq saw all these files as
belonging to the same namespace so it didn't really care where they
lived.

This could also imply a performance gain as we now effectively
traverse less directories when locating a library.

See also discussion in #10003

[doc] [dune] [ltac2] Build Ltac2 documentation [dune build system]

2020-01-17T17:02:33+00:00

This partially fixes #10139 ; we now build the Ltac2 documentation and
deploy it.

The fix here can be used for inspiration to do the make-based part.

[doc] also scan plugins/ to build the lirbary index

2018-11-07T11:23:06+00:00

Avoid scanning .coq-native directories when building the library index.

2014-06-26T15:37:29+00:00

Improved synchronisation of stdlib index page with current library state.

2012-02-01T08:57:47+00:00

- Made generation of index page fail if a file is missing in list or
  listed but unbound in existing theories
- Added a file hidden-files to optionally list library files not to show
  in the index page (though it is currently empty)
- Added directory Unicode (why not to have it after all?)

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

index-list.html.template: add missing files

2012-01-31T16:18:14+00:00

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

Move stuff about positive into a distinct PArith subdir

2010-11-02T14:44:08+00:00

 Beware! after this, a ./configure must be done. It might also
 be a good idea to chase any phantom .vo remaining after a make clean

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

Update of documentation for the standard library (cf. #2332)

2010-06-28T10:33:35+00:00

This is a slightly modified version of the patch proposed in #2332

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

Fix library index template and associated script.

2008-06-07T18:25:28+00:00

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