Merge PR #7406: Fix #7214: install knows which ml files do not get compiled to cmx.

3 files changed, 3 insertions, 160 deletions

diff --git a/Makefile.install b/Makefile.install
index ece271adc..010e35d42 100644
--- a/Makefile.install
+++ b/Makefile.install
@@ -97,7 +97,9 @@ INSTALLCMI = $(sort \
 	$(foreach lib,$(CORECMA), $(addsuffix .cmi,$($(lib:.cma=_MLLIB_DEPENDENCIES))))) \
 	$(PLUGINS:.cmo=.cmi)
 
-INSTALLCMX = $(sort $(filter-out checker/% ide/% tools/% dev/% configure.cmx, $(MLFILES:.ml=.cmx)))
+INSTALLCMX = $(sort $(filter-out checker/% ide/% tools/% dev/% \
+	configure.cmx toplevel/coqtop_byte_bin.cmx plugins/extraction/big.cmx, \
+	$(MLFILES:.ml=.cmx)))
 
 install-devfiles:
 	$(MKDIR) $(FULLBINDIR)
diff --git a/clib/deque.ml b/clib/deque.ml
deleted file mode 100644
index 9d0bbf12a..000000000
--- a/clib/deque.ml
+++ /dev/null
@@ -1,99 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <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)         *)
-(************************************************************************)
-
-exception Empty
-
-type 'a t = {
-  face : 'a list;
-  rear : 'a list;
-  lenf : int;
-  lenr : int;
-}
-
-let rec split i accu l = match l with
-| [] ->
-  if Int.equal i 0 then (accu, []) else invalid_arg "split"
-| t :: q ->
-  if Int.equal i 0 then (accu, l)
-  else split (pred i) (t :: accu) q
-
-let balance q =
-  let avg = (q.lenf + q.lenr) / 2 in
-  let dif = q.lenf + q.lenr - avg in
-  if q.lenf > succ (2 * q.lenr) then
-    let (ff, fr) = split avg [] q.face in
-    { face = List.rev ff ; rear = q.rear @ List.rev fr; lenf = avg; lenr = dif }
-  else if q.lenr > succ (2 * q.lenf) then
-    let (rf, rr) = split avg [] q.rear in
-    { face = q.face @ List.rev rr ; rear = List.rev rf; lenf = dif; lenr = avg }
-  else q
-
-let empty = {
-  face = [];
-  rear = [];
-  lenf = 0;
-  lenr = 0;
-}
-
-let lcons x q =
-  balance { q with lenf = succ q.lenf; face = x :: q.face }
-
-let lhd q = match q.face with
-| [] ->
-  begin match q.rear with
-  | [] -> raise Empty
-  | t :: _ -> t
-  end
-| t :: _ -> t
-
-let ltl q = match q.face with
-| [] ->
-  begin match q.rear with
-  | [] -> raise Empty
-  | t :: _ -> empty
-  end
-| t :: r -> balance { q with lenf = pred q.lenf; face = r }
-
-let rcons x q =
-  balance { q with lenr = succ q.lenr; rear = x :: q.rear }
-
-let rhd q = match q.rear with
-| [] ->
-  begin match q.face with
-  | [] -> raise Empty
-  | t :: r -> t
-  end
-| t :: _ -> t
-
-let rtl q = match q.rear with
-| [] ->
-  begin match q.face with
-  | [] -> raise Empty
-  | t :: r -> empty
-  end
-| t :: r ->
-  balance { q with lenr = pred q.lenr; rear = r }
-
-let rev q = {
-  face = q.rear;
-  rear = q.face;
-  lenf = q.lenr;
-  lenr = q.lenf;
-}
-
-let length q = q.lenf + q.lenr
-
-let is_empty q = Int.equal (length q) 0
-
-let filter f q =
-  let fold (accu, len) x = if f x then (x :: accu, succ len) else (accu, len) in
-  let (rf, lenf) = List.fold_left fold ([], 0) q.face in
-  let (rr, lenr) = List.fold_left fold ([], 0) q.rear in
-  balance { face = List.rev rf; rear = List.rev rr; lenf = lenf; lenr = lenr }
diff --git a/clib/deque.mli b/clib/deque.mli
deleted file mode 100644
index 1c03c384d..000000000
--- a/clib/deque.mli
+++ /dev/null
@@ -1,60 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <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)         *)
-(************************************************************************)
-
-(** * Purely functional, double-ended queues *)
-
-(** This module implements the banker's deque, from Okasaki. Most operations are
-    amortized O(1). *)
-
-type +'a t
-
-exception Empty
-
-(** {5 Constructor} *)
-
-val empty : 'a t
-
-(** The empty deque. *)
-
-(** {5 Left-side operations} *)
-
-val lcons : 'a -> 'a t -> 'a t
-(** Pushes an element on the left side of the deque. *)
-
-val lhd : 'a t -> 'a
-(** Returns the leftmost element in the deque. Raises [Empty] when empty. *)
-
-val ltl : 'a t -> 'a t
-(** Returns the left-tail of the deque. Raises [Empty] when empty. *)
-
-(** {5 Right-side operations} *)
-
-val rcons : 'a -> 'a t -> 'a t
-(** Same as [lcons] but on the right side. *)
-
-val rhd : 'a t -> 'a
-(** Same as [lhd] but on the right side. *)
-
-val rtl : 'a t -> 'a t
-(** Same as [ltl] but on the right side. *)
-
-(** {5 Operations} *)
-
-val rev : 'a t -> 'a t
-(** Reverse deque. *)
-
-val length : 'a t -> int
-(** Length of a deque. *)
-
-val is_empty : 'a t -> bool
-(** Emptyness of a deque. *)
-
-val filter : ('a -> bool) -> 'a t -> 'a t
-(** Filters the deque *)