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

diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v
deleted file mode 100644
index 6db62e8401..0000000000
--- a/plugins/micromega/VarMap.v
+++ /dev/null
@@ -1,79 +0,0 @@
-(* -*- coding: utf-8 -*- *)
-(************************************************************************)
-(*         *   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                             *)
-(*                                                                      *)
-(************************************************************************)
-
-Require Import ZArith_base.
-Require Import Coq.Arith.Max.
-Require Import List.
-Set Implicit Arguments.
-
-(* 
- * This adds a Leaf constructor to the varmap data structure (plugins/quote/Quote.v)
- * --- it is harmless and spares a lot of Empty.
- * It also means smaller proof-terms.
- * As a side note, by dropping the polymorphism, one gets small, yet noticeable, speed-up.
- *)
-
-Inductive t {A} : Type :=
-| Empty : t
-| Elt : A -> t
-| Branch : t  -> A -> t  -> t .
-Arguments t : clear implicits.
-
-Section MakeVarMap.
-  
-  Variable A : Type.
-  Variable default : A.
-
-  Notation t := (t A).
-
-  Fixpoint find (vm : t) (p:positive) {struct vm} : A :=
-    match vm with
-      | Empty => default
-      | Elt i => i
-      | Branch l e r => match p with
-                        | xH => e
-                        | xO p => find l p
-                        | xI p => find r p
-                      end
-    end.
-
-  Fixpoint singleton (x:positive) (v : A) : t :=
-    match x with
-    | xH => Elt v
-    | xO p => Branch (singleton p v) default Empty
-    | xI p => Branch Empty default (singleton p v)
-    end.
-  
-  Fixpoint vm_add (x: positive) (v : A) (m : t) {struct m} : t :=
-    match m with
-    | Empty   => singleton x v
-    | Elt vl =>
-      match x with
-      | xH => Elt v
-      | xO p => Branch (singleton p v) vl Empty
-      | xI p => Branch Empty vl (singleton p v)
-      end
-    | Branch l o r =>
-      match x with
-      | xH => Branch l v r
-      | xI p => Branch l o (vm_add p v r)
-      | xO p => Branch (vm_add p v l) o r
-      end
-    end.
-
-  
-End MakeVarMap.