aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-06-11 16:36:19 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-06-11 16:36:19 +0200
commit8a6fb588c400e8f656fe82c26ff754f41e746296 (patch)
treef61481f4caf89cd5c1b608e589c6c40b55806562
parent3a3464e0953bda9291bdc8078b0bad298109aa42 (diff)
parentdc14c5132d2e7578f0677ec0202308a38da0b1cd (diff)
Merge PR #7406: Fix #7214: install knows which ml files do not get compiled to cmx.
-rw-r--r--Makefile.install4
-rw-r--r--clib/deque.ml99
-rw-r--r--clib/deque.mli60
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 *)