From 8a9445fbf65d4ddf2c96348025d487b4d54a5d01 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 5 Jan 2016 19:36:02 +0100
Subject: Fix order of files in mllib.

CString was linked after Serialize, although the later was using CString.equal.
This had not been noticed so far because OCaml was ignoring functions marked as
external in interfaces (which is the case of CString.equal) when considering
link dependencies. This was changed on the OCaml side as part of the fix of
PR#6956, so linking was now failing in several places.
---
 Makefile.build        | 5 +++--
 checker/check.mllib   | 4 ++--
 dev/printers.mllib    | 4 ++--
 grammar/grammar.mllib | 4 ++--
 lib/clib.mllib        | 4 ++--
 5 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/Makefile.build b/Makefile.build
index 00ff6a7a4c..56fc5f0c7d 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -294,9 +294,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 49ca6bf051..0d36e3a0f1 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -17,6 +17,8 @@ Flags
 Control
 Pp_control
 Loc
+CList
+CString
 Serialize
 Stateid
 Feedback
@@ -25,8 +27,6 @@ Segmenttree
 Unicodetable
 Unicode
 CObj
-CList
-CString
 CArray
 CStack
 Util
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 07b48ed573..eeca6809ae 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -16,6 +16,8 @@ Backtrace
 IStream
 Pp_control
 Loc
+CList
+CString
 Compat
 Flags
 Control
@@ -28,8 +30,6 @@ Segmenttree
 Unicodetable
 Unicode
 CObj
-CList
-CString
 CArray
 CStack
 Util
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index 60ea0df026..71e5b8ae2c 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -16,13 +16,13 @@ Backtrace
 Pp_control
 Flags
 Loc
+CList
+CString
 Serialize
 Stateid
 Feedback
 Pp
 
-CList
-CString
 CArray
 CStack
 Util
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 7ff1d29359..9c9607abdb 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -18,11 +18,11 @@ Pp_control
 Flags
 Control
 Loc
+CList
+CString
 Serialize
 Deque
 CObj
-CList
-CString
 CArray
 CStack
 Util
-- 
cgit v1.2.3


From 64487121a35628512c1bd1b4e7039132f84ab270 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 5 Jan 2016 19:41:08 +0100
Subject: Avoid warning 31: test printer was linked twice with Dynlink and Str.

Linking a module twice is unsafe and warning 31 will be fatal by default in
OCaml 4.03. See PR#5461.
---
 Makefile.build | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/Makefile.build b/Makefile.build
index 56fc5f0c7d..d9090197a2 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
 
 
-- 
cgit v1.2.3


From ffc135337b479349a9e94c0da0a87531cf0684fa Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 5 Jan 2016 19:48:32 +0100
Subject: Disable warning 31 when generating coqtop from coqmktop.

In OCaml 3.x, the toploop of OCaml was accessible from toplevellib.cma. In
OCaml 4.x, it was replaced by compiler-libs. However, linking with
compiler-libs produces a warning (fatal with OCaml 4.03) as soon as we have a
file named errors.ml or lexer.ml...

The only satisfactory solution seems to be to "pack" compiler libs. But it is
not done currently in the OCaml distribution, and implementing it in coqmktop
at this point would be too risky. So for now, I am disabling the warning until
we hear from the OCaml team. In principle, this clash of modules names can
break OCaml's type safety, so we are living dangerously.
---
 tools/coqmktop.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
index be796e6956..e29cf60e36 100644
--- a/tools/coqmktop.ml
+++ b/tools/coqmktop.ml
@@ -280,7 +280,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
-- 
cgit v1.2.3


From 23cbf43f353c50fa72b72d694611c5c14367cea2 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 6 Jan 2016 00:58:42 +0100
Subject: Protect code against changes in Map interface.

The Map interface of upcoming OCaml 4.03 includes a new union operator. In
order to make our homemade implementation of Maps compatible with OCaml
versions from 3.12 to 4.03, we define our own signatures for Maps.
---
 checker/univ.mli               |  2 +-
 kernel/names.mli               | 10 +++++-----
 lib/cMap.ml                    |  2 +-
 lib/cMap.mli                   |  2 +-
 lib/cSig.mli                   | 31 +++++++++++++++++++++++++++++++
 library/goptions.mli           |  2 +-
 library/libnames.mli           |  2 +-
 plugins/cc/ccalgo.mli          |  6 +++---
 plugins/extraction/table.mli   |  2 +-
 plugins/firstorder/sequent.mli |  2 +-
 10 files changed, 46 insertions(+), 15 deletions(-)

diff --git a/checker/univ.mli b/checker/univ.mli
index 02c1bbdb91..f3216feac4 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/kernel/names.mli b/kernel/names.mli
index 7cc4443752..59419af2ef 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -395,7 +395,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
@@ -403,10 +403,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 cf590d96c3..048a690812 100644
--- a/lib/cMap.ml
+++ b/lib/cMap.ml
@@ -16,7 +16,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 23d3801e08..9d0fbbad24 100644
--- a/lib/cMap.mli
+++ b/lib/cMap.mli
@@ -18,7 +18,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 2a8bda2936..e095c82cb0 100644
--- a/lib/cSig.mli
+++ b/lib/cSig.mli
@@ -45,3 +45,34 @@ sig
 end
 (** Redeclaration of OCaml set signature, to preserve compatibility. See OCaml
     documentation for more information. *)
+
+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/library/goptions.mli b/library/goptions.mli
index 9d87c14c50..25b5315c2a 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 b95c088715..c72f517532 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 0dcf3a870f..34c19958a9 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 916cf3ad6b..4e638a0ace 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 dc3f05be69..760168c9f6 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
 
-- 
cgit v1.2.3


From 8b5d02d8706f99015c2ce8efcad32b7af228dd53 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 6 Jan 2016 11:32:31 +0100
Subject: Prevent coq_makefile from parsing project files in the reverse order.
 (Fix bug #4477)

The bug was a bit subtle. Function process_cmd_line can be called in three
different ways:
  1. tail-recursively to accumulate parsed options in reverse order,
  2. directly to parse a file (coqide) or a command line (coq_makefile),
  3. recursively to handle a "-f" option.
Once its execution finished, the function reversed its accumulator so
that the parsed options are in correct order. Due to the third case, this
means that the final local order of options was depending on the parity of
the depth of "-f" options. This commit fixes it by changing the function so
that the recursive call gets the actual accumulator rather than its
reversed version.

Warning: this will break all the projects that were inadvertently (or not)
relying on the bug. This might also require a further commit if
coq_makefile itself was relying on the bug.
---
 ide/project_file.ml4 | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/ide/project_file.ml4 b/ide/project_file.ml4
index 152f76cc0e..07ab5344d2 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
-- 
cgit v1.2.3