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

diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
deleted file mode 100644
index 0e8c09ef1b..0000000000
--- a/plugins/micromega/MExtraction.v
+++ /dev/null
@@ -1,66 +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)         *)
-(************************************************************************)
-(*                                                                      *)
-(* Micromega: A reflexive tactic using the Positivstellensatz           *)
-(*                                                                      *)
-(*  Frédéric Besson (Irisa/Inria) 2006-2008                             *)
-(*                                                                      *)
-(************************************************************************)
-
-(* Used to generate micromega.ml *)
-
-Require Extraction.
-Require Import ZMicromega.
-Require Import QMicromega.
-Require Import RMicromega.
-Require Import VarMap.
-Require Import RingMicromega.
-Require Import NArith.
-Require Import QArith.
-
-Extract Inductive prod => "( * )" [ "(,)" ].
-Extract Inductive list => list [ "[]" "(::)" ].
-Extract Inductive bool => bool [ true false ].
-Extract Inductive sumbool => bool [ true false ].
-Extract Inductive option => option [ Some None ].
-Extract Inductive sumor => option [ Some None ].
-(** Then, in a ternary alternative { }+{ }+{ },
-   -  leftmost choice (Inleft Left) is (Some true),
-   -  middle choice (Inleft Right) is (Some false),
-   -  rightmost choice (Inright) is (None) *)
-
-
-(** To preserve its laziness, andb is normally expanded.
-    Let's rather use the ocaml && *)
-Extract Inlined Constant andb => "(&&)".
-
-Import Reals.Rdefinitions.
-
-Extract Constant R => "int".
-Extract Constant R0 => "0".
-Extract Constant R1 => "1".
-Extract Constant Rplus => "( + )".
-Extract Constant Rmult => "( * )".
-Extract Constant Ropp  => "fun x -> - x".
-Extract Constant Rinv   => "fun x -> 1 / x".
-
-(** In order to avoid annoying build dependencies the actual
-    extraction is only performed as a test in the test suite. *)
-(*Extraction "micromega.ml"
-           Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula
-           Tauto.abst_form
-           ZMicromega.cnfZ  ZMicromega.Zeval_const QMicromega.cnfQ
-           List.map simpl_cone (*map_cone  indexes*)
-           denorm Qpower vm_add
-   normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
-*)
-(* Local Variables: *)
-(* coding: utf-8 *)
-(* End: *)