aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.build10
-rw-r--r--checker/check.mllib4
-rw-r--r--checker/univ.mli2
-rw-r--r--dev/printers.mllib4
-rw-r--r--grammar/grammar.mllib4
-rw-r--r--ide/project_file.ml46
-rw-r--r--kernel/names.mli10
-rw-r--r--lib/cMap.ml2
-rw-r--r--lib/cMap.mli2
-rw-r--r--lib/cSig.mli31
-rw-r--r--lib/clib.mllib4
-rw-r--r--library/goptions.mli2
-rw-r--r--library/libnames.mli2
-rw-r--r--plugins/cc/ccalgo.mli6
-rw-r--r--plugins/extraction/table.mli2
-rw-r--r--plugins/firstorder/sequent.mli2
-rw-r--r--tools/coqmktop.ml2
17 files changed, 66 insertions, 29 deletions
diff --git a/Makefile.build b/Makefile.build
index a3766a50f..9d4f56e2a 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -132,10 +132,11 @@ SYSMOD:=str unix dynlink threads
SYSCMA:=$(addsuffix .cma,$(SYSMOD))
SYSCMXA:=$(addsuffix .cmxa,$(SYSMOD))
+# We do not repeat the dependencies already in SYSMOD here
ifeq ($(CAMLP4),camlp5)
-P4CMA:=gramlib.cma str.cma
+P4CMA:=gramlib.cma
else
-P4CMA:=dynlink.cma camlp4lib.cma str.cma
+P4CMA:=camlp4lib.cma
endif
@@ -294,9 +295,10 @@ checker/check.cmxa: | md5chk checker/check.mllib.d
# Csdp to micromega special targets
###########################################################################
-plugins/micromega/csdpcert$(EXE): $(CSDPCERTCMO:.cmo=$(BESTOBJ))
+plugins/micromega/csdpcert$(EXE): $(CSDPCERTCMO:.cmo=$(BESTOBJ)) \
+ $(addsuffix $(BESTLIB), lib/clib)
$(SHOW)'OCAMLBEST -o $@'
- $(HIDE)$(call bestocaml,,nums unix)
+ $(HIDE)$(call bestocaml,,nums unix clib)
###########################################################################
# CoqIde special targets
diff --git a/checker/check.mllib b/checker/check.mllib
index a029b0245..3725989e8 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -18,6 +18,8 @@ Flags
Control
Pp_control
Loc
+CList
+CString
Serialize
Stateid
Feedback
@@ -26,8 +28,6 @@ Segmenttree
Unicodetable
Unicode
CObj
-CList
-CString
CArray
CStack
Util
diff --git a/checker/univ.mli b/checker/univ.mli
index 02c1bbdb9..f3216feac 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -130,7 +130,7 @@ val check_constraints : constraints -> universes -> bool
(** {6 Support for universe polymorphism } *)
(** Polymorphic maps from universe levels to 'a *)
-module LMap : Map.S with type key = universe_level
+module LMap : CSig.MapS with type key = universe_level
module LSet : CSig.SetS with type elt = universe_level
type 'a universe_map = 'a LMap.t
diff --git a/dev/printers.mllib b/dev/printers.mllib
index b498c2659..7f9da4eab 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -17,6 +17,8 @@ Backtrace
IStream
Pp_control
Loc
+CList
+CString
Compat
Flags
Control
@@ -29,8 +31,6 @@ Segmenttree
Unicodetable
Unicode
CObj
-CList
-CString
CArray
CStack
Util
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index b167643d3..6098de8f0 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -17,13 +17,13 @@ Backtrace
Pp_control
Flags
Loc
+CList
+CString
Serialize
Stateid
Feedback
Pp
-CList
-CString
CArray
CStack
Util
diff --git a/ide/project_file.ml4 b/ide/project_file.ml4
index 152f76cc0..07ab5344d 100644
--- a/ide/project_file.ml4
+++ b/ide/project_file.ml4
@@ -48,7 +48,7 @@ let parse f =
res
let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts) l = function
- | [] -> opts,List.rev l
+ | [] -> opts, l
| ("-h"|"--help") :: _ ->
raise Parsing_error
| ("-no-opt"|"-byte") :: r ->
@@ -128,6 +128,10 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts)
else if (Filename.check_suffix f ".mlpack") then MLPACK f
else Subdir f) :: l) r
+let process_cmd_line orig_dir opts l args =
+ let (opts, l) = process_cmd_line orig_dir opts l args in
+ opts, List.rev l
+
let rec post_canonize f =
if Filename.basename f = Filename.current_dir_name
then let dir = Filename.dirname f in
diff --git a/kernel/names.mli b/kernel/names.mli
index b128fe335..38a51a392 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -409,7 +409,7 @@ end
module Mindset : CSig.SetS with type elt = MutInd.t
module Mindmap : Map.ExtS with type key = MutInd.t and module Set := Mindset
-module Mindmap_env : Map.S with type key = MutInd.t
+module Mindmap_env : CSig.MapS with type key = MutInd.t
(** Beware: first inductive has index 0 *)
type inductive = MutInd.t * int
@@ -417,10 +417,10 @@ type inductive = MutInd.t * int
(** Beware: first constructor has index 1 *)
type constructor = inductive * int
-module Indmap : Map.S with type key = inductive
-module Constrmap : Map.S with type key = constructor
-module Indmap_env : Map.S with type key = inductive
-module Constrmap_env : Map.S with type key = constructor
+module Indmap : CSig.MapS with type key = inductive
+module Constrmap : CSig.MapS with type key = constructor
+module Indmap_env : CSig.MapS with type key = inductive
+module Constrmap_env : CSig.MapS with type key = constructor
val ind_modpath : inductive -> ModPath.t
val constr_modpath : constructor -> ModPath.t
diff --git a/lib/cMap.ml b/lib/cMap.ml
index 876f84736..925af00c0 100644
--- a/lib/cMap.ml
+++ b/lib/cMap.ml
@@ -23,7 +23,7 @@ module type S = Map.S
module type ExtS =
sig
- include Map.S
+ include CSig.MapS
module Set : CSig.SetS with type elt = key
val update : key -> 'a -> 'a t -> 'a t
val modify : key -> (key -> 'a -> 'a) -> 'a t -> 'a t
diff --git a/lib/cMap.mli b/lib/cMap.mli
index cd3d2f5b1..f032a6d7d 100644
--- a/lib/cMap.mli
+++ b/lib/cMap.mli
@@ -25,7 +25,7 @@ module type S = Map.S
module type ExtS =
sig
- include Map.S
+ include CSig.MapS
(** The underlying Map library *)
module Set : CSig.SetS with type elt = key
diff --git a/lib/cSig.mli b/lib/cSig.mli
index 796e58cbf..151cfbdca 100644
--- a/lib/cSig.mli
+++ b/lib/cSig.mli
@@ -49,3 +49,34 @@ end
documentation for more information. *)
module type EmptyS = sig end
+
+module type MapS =
+sig
+ type key
+ type (+'a) t
+ val empty: 'a t
+ val is_empty: 'a t -> bool
+ val mem: key -> 'a t -> bool
+ val add: key -> 'a -> 'a t -> 'a t
+ val singleton: key -> 'a -> 'a t
+ val remove: key -> 'a t -> 'a t
+ val merge:
+ (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
+ val compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
+ val equal: ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
+ val iter: (key -> 'a -> unit) -> 'a t -> unit
+ val fold: (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+ val for_all: (key -> 'a -> bool) -> 'a t -> bool
+ val exists: (key -> 'a -> bool) -> 'a t -> bool
+ val filter: (key -> 'a -> bool) -> 'a t -> 'a t
+ val partition: (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
+ val cardinal: 'a t -> int
+ val bindings: 'a t -> (key * 'a) list
+ val min_binding: 'a t -> (key * 'a)
+ val max_binding: 'a t -> (key * 'a)
+ val choose: 'a t -> (key * 'a)
+ val split: key -> 'a t -> 'a t * 'a option * 'a t
+ val find: key -> 'a t -> 'a
+ val map: ('a -> 'b) -> 'a t -> 'b t
+ val mapi: (key -> 'a -> 'b) -> 'a t -> 'b t
+end
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 1770df199..3c1c5da33 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -19,11 +19,11 @@ Pp_control
Flags
Control
Loc
+CList
+CString
Serialize
Deque
CObj
-CList
-CString
CArray
CStack
Util
diff --git a/library/goptions.mli b/library/goptions.mli
index 9d87c14c5..25b5315c2 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -133,7 +133,7 @@ val declare_stringopt_option: string option option_sig -> string option write_fu
(** {6 Special functions supposed to be used only in vernacentries.ml } *)
-module OptionMap : Map.S with type key = option_name
+module OptionMap : CSig.MapS with type key = option_name
val get_string_table :
option_name ->
diff --git a/library/libnames.mli b/library/libnames.mli
index b95c08871..c72f51753 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -60,7 +60,7 @@ val path_of_string : string -> full_path
val string_of_path : full_path -> string
val pr_path : full_path -> std_ppcmds
-module Spmap : Map.S with type key = full_path
+module Spmap : CSig.MapS with type key = full_path
val restrict_path : int -> full_path -> full_path
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 0dcf3a870..34c19958a 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -20,8 +20,8 @@ type pa_fun=
fnargs:int}
-module PafMap : Map.S with type key = pa_fun
-module PacMap : Map.S with type key = pa_constructor
+module PafMap : CSig.MapS with type key = pa_fun
+module PacMap : CSig.MapS with type key = pa_constructor
type cinfo =
{ci_constr: pconstructor; (* inductive type *)
@@ -185,7 +185,7 @@ val empty_forest: unit -> forest
(*type pa_constructor
-module PacMap:Map.S with type key=pa_constructor
+module PacMap:CSig.MapS with type key=pa_constructor
type term =
Symb of Term.constr
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 916cf3ad6..4e638a0ac 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -13,7 +13,7 @@ open Miniml
open Declarations
module Refset' : CSig.SetS with type elt = global_reference
-module Refmap' : Map.S with type key = global_reference
+module Refmap' : CSig.MapS with type key = global_reference
val safe_basename_of_global : global_reference -> Id.t
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index dc3f05be6..760168c9f 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -13,7 +13,7 @@ open Globnames
module OrderedConstr: Set.OrderedType with type t=constr
-module CM: Map.S with type key=constr
+module CM: CSig.MapS with type key=constr
type h_item = global_reference * (int*constr) option
diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
index a6254b2a4..d2780e763 100644
--- a/tools/coqmktop.ml
+++ b/tools/coqmktop.ml
@@ -279,7 +279,7 @@ let main () =
(* - We add topstart.cmo explicitly because we shunted ocamlmktop wrapper.
- With the coq .cma, we MUST use the -linkall option. *)
let args =
- "-linkall" :: "-rectypes" :: flags @ copts @ options @
+ "-linkall" :: "-rectypes" :: "-w" :: "-31" :: flags @ copts @ options @
(std_includes basedir) @ tolink @ [ main_file ] @ topstart
in
if !echo then begin
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 06:22:31 +0000