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

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

1 files changed, 0 insertions, 56 deletions

diff --git a/plugins/extraction/ExtrOCamlInt63.v b/plugins/extraction/ExtrOCamlInt63.v
deleted file mode 100644
index a2ee602313..0000000000
--- a/plugins/extraction/ExtrOCamlInt63.v
+++ /dev/null
@@ -1,56 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** Extraction to OCaml of native 63-bit machine integers. *)
-
-From Coq Require Int63 Extraction.
-
-(** Basic data types used by some primitive operators. *)
-
-Extract Inductive bool => bool [ true false ].
-Extract Inductive prod => "( * )" [ "" ].
-Extract Inductive comparison => int [ "0" "(-1)" "1" ].
-Extract Inductive DoubleType.carry => "Uint63.carry" [ "Uint63.C0" "Uint63.C1" ].
-
-(** Primitive types and operators. *)
-Extract Constant Int63.int => "Uint63.t".
-Extraction Inline Int63.int.
-(* Otherwise, the name conflicts with the primitive OCaml type [int] *)
-
-Extract Constant Int63.lsl => "Uint63.l_sl".
-Extract Constant Int63.lsr => "Uint63.l_sr".
-Extract Constant Int63.land => "Uint63.l_and".
-Extract Constant Int63.lor => "Uint63.l_or".
-Extract Constant Int63.lxor => "Uint63.l_xor".
-
-Extract Constant Int63.add => "Uint63.add".
-Extract Constant Int63.sub => "Uint63.sub".
-Extract Constant Int63.mul => "Uint63.mul".
-Extract Constant Int63.mulc => "Uint63.mulc".
-Extract Constant Int63.div => "Uint63.div".
-Extract Constant Int63.mod => "Uint63.rem".
-
-Extract Constant Int63.eqb => "Uint63.equal".
-Extract Constant Int63.ltb => "Uint63.lt".
-Extract Constant Int63.leb => "Uint63.le".
-
-Extract Constant Int63.addc => "Uint63.addc".
-Extract Constant Int63.addcarryc => "Uint63.addcarryc".
-Extract Constant Int63.subc => "Uint63.subc".
-Extract Constant Int63.subcarryc => "Uint63.subcarryc".
-
-Extract Constant Int63.diveucl => "Uint63.diveucl".
-Extract Constant Int63.diveucl_21 => "Uint63.div21".
-Extract Constant Int63.addmuldiv => "Uint63.addmuldiv".
-
-Extract Constant Int63.compare => "Uint63.compare".
-
-Extract Constant Int63.head0 => "Uint63.head0".
-Extract Constant Int63.tail0 => "Uint63.tail0".