[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, 46 deletions

diff --git a/plugins/setoid_ring/Ring.v b/plugins/setoid_ring/Ring.v
deleted file mode 100644
index 35e308565f..0000000000
--- a/plugins/setoid_ring/Ring.v
+++ /dev/null
@@ -1,46 +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)         *)
-(************************************************************************)
-
-Require Import Bool.
-Require Export Ring_theory.
-Require Export Ring_base.
-Require Export InitialRing.
-Require Export Ring_tac.
-
-Lemma BoolTheory :
-  ring_theory false true xorb andb xorb (fun b:bool => b) (eq(A:=bool)).
-split; simpl.
-destruct x; reflexivity.
-destruct x; destruct y; reflexivity.
-destruct x; destruct y; destruct z; reflexivity.
-reflexivity.
-destruct x; destruct y; reflexivity.
-destruct x; destruct y; reflexivity.
-destruct x; destruct y; destruct z; reflexivity.
-reflexivity.
-destruct x; reflexivity.
-Qed.
-
-Definition bool_eq (b1 b2:bool) :=
-  if b1 then b2 else negb b2.
-
-Lemma bool_eq_ok : forall b1 b2, bool_eq b1 b2 = true -> b1 = b2.
-destruct b1; destruct b2; auto.
-Qed.
-
-Ltac bool_cst t :=
-  let t := eval hnf in t in
-  match t with
-    true => constr:(true)
-  | false => constr:(false)
-  | _ => constr:(NotConstant)
-  end.
-
-Add Ring bool_ring : BoolTheory (decidable bool_eq_ok, constants [bool_cst]).