diff options
-rw-r--r-- | Makefile.build | 10 | ||||
-rw-r--r-- | checker/check.mllib | 4 | ||||
-rw-r--r-- | checker/univ.mli | 2 | ||||
-rw-r--r-- | dev/printers.mllib | 4 | ||||
-rw-r--r-- | grammar/grammar.mllib | 4 | ||||
-rw-r--r-- | ide/project_file.ml4 | 6 | ||||
-rw-r--r-- | kernel/names.mli | 10 | ||||
-rw-r--r-- | lib/cMap.ml | 2 | ||||
-rw-r--r-- | lib/cMap.mli | 2 | ||||
-rw-r--r-- | lib/cSig.mli | 31 | ||||
-rw-r--r-- | lib/clib.mllib | 4 | ||||
-rw-r--r-- | library/goptions.mli | 2 | ||||
-rw-r--r-- | library/libnames.mli | 2 | ||||
-rw-r--r-- | plugins/cc/ccalgo.mli | 6 | ||||
-rw-r--r-- | plugins/extraction/table.mli | 2 | ||||
-rw-r--r-- | plugins/firstorder/sequent.mli | 2 | ||||
-rw-r--r-- | tools/coqmktop.ml | 2 |
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 |