From e525e2d3246c2540018f38e939ac784277ba1147 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 15 Apr 2015 11:01:19 +0200
Subject: Documenting the recommandation of toplevel-only commands.

---
 doc/refman/RefMan-oth.tex | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 4952ed7785..7d7a4c9a0c 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -680,7 +680,8 @@ should use the command \texttt{Locate File} (see Section~\ref{Locate File})
 
 Loadpaths are preferably managed using {\Coq} command line options
 (see Section~\ref{loadpath}) but there remain vernacular commands to
-manage them.
+manage them for practical puposes. Such commands are only meant to be issued in
+the toplevel, and using them in source files is discouraged.
 
 \subsection[\tt Pwd.]{\tt Pwd.\comindex{Pwd}\label{Pwd}}
 This command displays the current working directory.
-- 
cgit v1.2.3


From f9580dfa7bc89d0ca4c9d8b69d5f4b42d558234e Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 15 Apr 2015 13:51:38 +0200
Subject: Remove dirty debug printing from funind.

---
 plugins/funind/invfun.ml | 2 --
 1 file changed, 2 deletions(-)

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d9ae87ecc1..d10924f886 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -378,7 +378,6 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	    observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres)));
 	    (* Conclusion *)
 	    observe_tac "exact" (fun g ->
-				 Pp.msgnl (str "TITI " ++ pf_apply Printer.pr_lconstr_env g (app_constructor g));
 				 Proofview.V82.of_tactic (exact_check (app_constructor g)) g)  
 	  ]
       )
@@ -427,7 +426,6 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
       in
       (params_bindings@lemmas_bindings)
     in
-    Pp.msgnl (str "princ_type := " ++ pf_apply Printer.pr_lconstr_env g princ_type);
     tclTHENSEQ
       [ 
 	observe_tac "principle" (Proofview.V82.of_tactic (assert_by
-- 
cgit v1.2.3


From 92e491097dbd7ca610ded20c3c4a3bb978c996eb Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 16 Apr 2015 11:07:29 +0200
Subject: configure: fix paths on cygwin

Long story short: Filname.concat and other OCaml provided functions
to be "cross platform" don't work for us for two reasons:
1. their behavior is fixed when one compiles ocaml, not when one runs it
2. the build system of Coq is unix only

What is wrong with 1 is that if one compiles ocaml for windows
without requiring cygwin.dll (a good thing, since you don't need to
have cygwin to run ocaml) then the runtime always uses \
as dir_sep, no matter if you are running ocaml from a cygwin shell.
If you use \ as a dir separaton in cygwin command lines, without
going trough the cygpath "mangler", then things go wrong.

The second point is that the makefiles we have need a unix like
environment (e.g. we call sed).  So you can't compile Coq without
cygwin, unless you use a different build system, that is not what
we support (1 build system is enough work already, IMO).

To sum up: Running coq/ocaml requires no cygwin, comipling coq requires
a unix like shell, hence paths shall be unix like in configure/build stuff.
---
 configure.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/configure.ml b/configure.ml
index 9ff483603c..0169dffa9c 100644
--- a/configure.ml
+++ b/configure.ml
@@ -27,7 +27,7 @@ let die msg = eprintf "%s\nConfiguration script failed!\n" msg; exit 1
 
 let s2i = int_of_string
 let i2s = string_of_int
-let (/) = Filename.concat
+let (/) x y = x ^ "/" ^ y
 
 (** Remove the final '\r' that may exists on Win32 *)
 
-- 
cgit v1.2.3


From dfb64dda51f7eea174e41129c8d2e0c3559298ec Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 16 Apr 2015 08:35:57 +0200
Subject: Fixing bug #4190.

The solution is a bit ugly. In order for two tactic notations identifiers not
to be confused by the inclusion from two distinct modules, we embed the name of
the source module in the identifiers. This may still fail if the same module is
included twice with two distinct parameters, but this should not be possible
thanks to the fact any definition in there will forbid the inclusion, for it
would be repeated. People including twice the same empty module otherwise
probably deserve whatever will arise from it.
---
 kernel/names.ml        |  9 +++++++--
 kernel/names.mli       |  6 +++++-
 toplevel/metasyntax.ml | 18 +++++++++++++-----
 3 files changed, 25 insertions(+), 8 deletions(-)

diff --git a/kernel/names.ml b/kernel/names.ml
index 4ccf5b60ae..480b37e897 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -33,9 +33,9 @@ struct
 
   let hash = String.hash
 
-  let check_soft x =
+  let check_soft ?(warn = true) x =
     let iter (fatal, x) =
-      if fatal then Errors.error x else Pp.msg_warning (str x)
+      if fatal then Errors.error x else if warn then Pp.msg_warning (str x)
     in
     Option.iter iter (Unicode.ident_refutation x)
 
@@ -48,6 +48,11 @@ struct
     let s = String.copy s in
     String.hcons s
 
+  let of_string_soft s =
+    let () = check_soft ~warn:false s in
+    let s = String.copy s in
+    String.hcons s
+
   let to_string id = String.copy id
 
   let print id = str id
diff --git a/kernel/names.mli b/kernel/names.mli
index d82043da1a..92ee58f260 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -29,7 +29,11 @@ sig
 
   val of_string : string -> t
   (** Converts a string into an identifier. May raise [UserError _] if the
-      string is not valid. *)
+      string is not valid, or echo a warning if it contains invalid identifier
+      characters. *)
+
+  val of_string_soft : string -> t
+  (** Same as {!of_string} except that no warning is ever issued. *)
 
   val to_string : t -> string
   (** Converts a identifier into an string. *)
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index c8eff59b15..639ec1e6e3 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -62,11 +62,19 @@ let rec make_tags = function
   | [] -> []
 
 let make_fresh_key =
-  let id = Summary.ref ~name:"Tactic Notation counter" 0 in
-  fun () -> KerName.make
-    (Safe_typing.current_modpath (Global.safe_env ()))
-    (Global.current_dirpath ())
-    (incr id; Label.make ("_" ^ string_of_int !id))
+  let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in
+  fun () ->
+    let cur = incr id; !id in
+    let lbl = Id.of_string ("_" ^ string_of_int cur) in
+    let kn = Lib.make_kn lbl in
+    let (mp, dir, _) = KerName.repr kn in
+    (** We embed the full path of the kernel name in the label so that the
+        identifier should be unique. This ensures that including two modules
+        together won't confuse the corresponding labels. *)
+    let lbl = Id.of_string_soft (Printf.sprintf "%s#%s#%i"
+      (ModPath.to_string mp) (DirPath.to_string dir) cur)
+    in
+    KerName.make mp dir (Label.of_id lbl)
 
 type tactic_grammar_obj = {
   tacobj_key : KerName.t;
-- 
cgit v1.2.3


From f550af8ae4385f59965d2a421173a9a7feec9afa Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 16 Apr 2015 14:59:25 +0200
Subject: Test for bug #4190.

---
 test-suite/bugs/closed/4190.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 test-suite/bugs/closed/4190.v

diff --git a/test-suite/bugs/closed/4190.v b/test-suite/bugs/closed/4190.v
new file mode 100644
index 0000000000..2843488ba0
--- /dev/null
+++ b/test-suite/bugs/closed/4190.v
@@ -0,0 +1,15 @@
+Module Type A .
+ Tactic Notation "bar" := idtac "ITSME".
+End A.
+
+Module Type B.
+ Tactic Notation "foo" := fail "NOTME".
+End B.
+
+Module Type C := A <+ B.
+
+Module Type F (Import M : C).
+
+Lemma foo : True.
+Proof.
+bar.
-- 
cgit v1.2.3


From 820a453c158006244f02e079d1a820f6670a1293 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 16 Apr 2015 17:03:41 +0200
Subject: Ensuring purity of datastructures in the API.

---
 tactics/btermdn.ml  |  2 +-
 tactics/btermdn.mli |  2 +-
 tactics/dn.ml       |  2 +-
 tactics/dn.mli      |  2 +-
 tactics/hints.ml    | 16 +++++++++-------
 5 files changed, 13 insertions(+), 11 deletions(-)

diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 1f5177c3d5..b87d657539 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -144,7 +144,7 @@ struct
 
  type t = Dn.t
 
-  let create = Dn.create
+  let empty = Dn.empty
 
   let add = function
     | None ->
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index 6c396b4c8b..f29d186153 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -28,7 +28,7 @@ module Make :
 sig
   type t
 
-  val create : unit ->  t
+  val empty : t
 
   val add : transparent_state option -> t -> (constr_pattern * Z.t) -> t
   val rmv : transparent_state option -> t -> (constr_pattern * Z.t) -> t
diff --git a/tactics/dn.ml b/tactics/dn.ml
index 3b1614d6ce..aed2c28323 100644
--- a/tactics/dn.ml
+++ b/tactics/dn.ml
@@ -38,7 +38,7 @@ struct
 
   type  t = Trie.t
 
-  let create () = Trie.empty
+  let empty = Trie.empty
 
 (* [path_of dna pat] returns the list of nodes of the pattern [pat] read in
 prefix ordering, [dna] is the function returning the main node of a pattern *)
diff --git a/tactics/dn.mli b/tactics/dn.mli
index 20407e9d97..2a60c3eb82 100644
--- a/tactics/dn.mli
+++ b/tactics/dn.mli
@@ -10,7 +10,7 @@ sig
 
   type t
 
-  val create : unit -> t
+  val empty : t
 
   (** [add t f (tree,inf)] adds a structured object [tree] together with
      the associated information [inf] to the table [t]; the function
diff --git a/tactics/hints.ml b/tactics/hints.ml
index dea47794ec..55d62e1514 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -171,7 +171,7 @@ type search_entry = {
 let empty_se = {
   sentry_nopat = [];
   sentry_pat = [];
-  sentry_bnet = Bounded_net.create ();
+  sentry_bnet = Bounded_net.empty;
   sentry_mode = [];
 }
 
@@ -206,7 +206,7 @@ let rebuild_dn st se =
   let dn' = 
     List.fold_left 
       (fun dn (id, t) -> Bounded_net.add (Some st) dn (Option.get t.pat, (id, t)))
-      (Bounded_net.create ()) se.sentry_pat
+      Bounded_net.empty se.sentry_pat
   in
   { se with sentry_bnet = dn' }
 
@@ -394,7 +394,7 @@ module Hint_db = struct
     hintdb_state : Names.transparent_state;
     hintdb_cut : hints_path;
     hintdb_unfolds : Id.Set.t * Cset.t;
-    mutable hintdb_max_id : int;
+    hintdb_max_id : int;
     use_dn : bool;
     hintdb_map : search_entry Constr_map.t;
     (* A list of unindexed entries starting with an unfoldable constant
@@ -402,8 +402,9 @@ module Hint_db = struct
     hintdb_nopat : (global_reference option * stored_data) list
   }
 
-  let next_hint_id t = 
-    let h = t.hintdb_max_id in t.hintdb_max_id <- succ t.hintdb_max_id; h
+  let next_hint_id db =
+    let h = db.hintdb_max_id in
+    { db with hintdb_max_id = succ db.hintdb_max_id }, h
 
   let empty st use_dn = { hintdb_state = st;
 			  hintdb_cut = PathEmpty;
@@ -510,8 +511,9 @@ module Hint_db = struct
 	    state, { db with hintdb_unfolds = unfs }, true
       | _ -> db.hintdb_state, db, false
     in
-    let db = if db.use_dn && rebuild then rebuild_db st' db else db
-    in addkv k (next_hint_id db) v db
+    let db = if db.use_dn && rebuild then rebuild_db st' db else db in
+    let db, id = next_hint_id db in
+    addkv k id v db
 
   let add_list l db = List.fold_left (fun db k -> add_one k db) db l
 
-- 
cgit v1.2.3


From e7bc24af330f003f7a672b2a27c37ba001e70b2b Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 17 Apr 2015 12:45:14 +0200
Subject: No longer add dev/ to the LoadPath, only to the ML path.

This patch should get rid of the following warning:

  Invalid character '-' in identifier "v8-syntax".
---
 toplevel/coqinit.ml | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index db77877efd..f1d8a4923c 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -57,11 +57,6 @@ let load_rcfile() =
   else
     Flags.if_verbose msg_info (str"Skipping rcfile loading.")
 
-(* Puts dir in the path of ML and in the LoadPath *)
-let coq_add_path unix_path s =
-  Mltop.add_rec_path ~unix_path ~coq_root:(Names.DirPath.make [Nameops.coq_root;Names.Id.of_string s]) ~implicit:true;
-  Mltop.add_ml_dir unix_path
-
 (* Recursively puts dir in the LoadPath if -nois was not passed *)
 let add_stdlib_path ~unix_path ~coq_root ~with_ml =
   Mltop.add_rec_path ~unix_path ~coq_root ~implicit:(!Flags.load_init);
@@ -88,10 +83,11 @@ let init_load_path () =
   let coq_root = Names.DirPath.make [Nameops.coq_root] in
     (* NOTE: These directories are searched from last to first *)
     (* first, developer specific directory to open *)
-    if Coq_config.local then coq_add_path (coqlib/"dev") "dev";
+    if Coq_config.local then
+      Mltop.add_ml_dir (coqlib/"dev");
     (* main loops *)
     if Coq_config.local || !Flags.boot then begin
-      let () = Mltop.add_ml_dir (coqlib/"stm") in
+      Mltop.add_ml_dir (coqlib/"stm");
       Mltop.add_ml_dir (coqlib/"ide")
     end;
     Mltop.add_ml_dir (coqlib/"toploop");
-- 
cgit v1.2.3


From ec462f70ae8062696d4aec8b89c1bb5da3f6a19a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 1 Apr 2015 21:32:38 +0200
Subject: Fixing a few typos + some uniformization of writing in doc.

---
 doc/refman/RefMan-oth.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 7d7a4c9a0c..0a28a93a41 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -680,7 +680,7 @@ should use the command \texttt{Locate File} (see Section~\ref{Locate File})
 
 Loadpaths are preferably managed using {\Coq} command line options
 (see Section~\ref{loadpath}) but there remain vernacular commands to
-manage them for practical puposes. Such commands are only meant to be issued in
+manage them for practical purposes. Such commands are only meant to be issued in
 the toplevel, and using them in source files is discouraged.
 
 \subsection[\tt Pwd.]{\tt Pwd.\comindex{Pwd}\label{Pwd}}
-- 
cgit v1.2.3


From 1c0a1dbfd13f0618b33213c4d42e50d44465c987 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 17 Apr 2015 15:36:11 +0200
Subject: Extra fix to 934761875 and f4ee7ee31e4 on optimizing Import of
 several libraries at once (see #4193).

---
 library/library.ml            | 7 ++++++-
 test-suite/bugs/closed/4193.v | 7 +++++++
 2 files changed, 13 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/4193.v

diff --git a/library/library.ml b/library/library.ml
index 9d0ccb972a..b4261309fd 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -633,7 +633,12 @@ let import_module export modl =
           with Not_found-> flush acc; safe_locate_module m, [] in
         (match m with
         | MPfile dir -> aux (dir::acc) l
-        | mp -> flush acc; Declaremods.import_module export mp; aux [] l)
+        | mp ->
+            flush acc;
+            try Declaremods.import_module export mp; aux [] l
+            with Not_found ->
+              user_err_loc (loc,"import_library",
+                str ((string_of_qualid dir)^" is not a module")))
     | [] -> flush acc
   in aux [] modl
 
diff --git a/test-suite/bugs/closed/4193.v b/test-suite/bugs/closed/4193.v
new file mode 100644
index 0000000000..885d04a927
--- /dev/null
+++ b/test-suite/bugs/closed/4193.v
@@ -0,0 +1,7 @@
+Module Type E.
+End E.
+
+Module Type A (M : E).
+End A.
+
+Fail Module Type F (Import X : A).
-- 
cgit v1.2.3


From 1bb47bf8f5d435b33b2bf5bd234e3eae372d99f6 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 17 Apr 2015 18:14:52 +0200
Subject: 8.5beta2 release.

---
 configure.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/configure.ml b/configure.ml
index 0169dffa9c..bbe4352080 100644
--- a/configure.ml
+++ b/configure.ml
@@ -11,8 +11,8 @@
 #load "str.cma"
 open Printf
 
-let coq_version = "8.5beta1"
-let coq_macos_version = "8.5.91" (** "[...] should be a string comprised of
+let coq_version = "8.5beta2"
+let coq_macos_version = "8.4.92" (** "[...] should be a string comprised of
 three non-negative, period-separed integers [...]" *)
 let vo_magic = 8591
 let state_magic = 58501
-- 
cgit v1.2.3


From 738551a294d5d8393253568764f9bea4cf45f7c5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 19 Apr 2015 12:39:37 +0200
Subject: Slightly more efficient implementation of the logic monad.

We just inline the state in the iolist: less closures makes the GC happier.
---
 proofs/logic_monad.ml | 120 +++++++++++++++++++++++---------------------------
 1 file changed, 56 insertions(+), 64 deletions(-)

diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml
index d509670ec2..cb3e5a1860 100644
--- a/proofs/logic_monad.ml
+++ b/proofs/logic_monad.ml
@@ -208,118 +208,110 @@ struct
   type rich_exn = Exninfo.iexn
 
   type 'a iolist =
-      { iolist : 'r. (rich_exn -> 'r NonLogical.t) ->
-                     ('a -> (rich_exn -> 'r NonLogical.t) -> 'r NonLogical.t) ->
-                     'r NonLogical.t }
+    { iolist : 'r. state -> (rich_exn -> 'r NonLogical.t) ->
+      ('a -> state -> (rich_exn -> 'r NonLogical.t) -> 'r NonLogical.t) ->
+      'r NonLogical.t }
 
   include Monad.Make(struct
-    type 'a t = state -> ('a * state) iolist
 
-    let return x : 'a t = (); fun s ->
-      { iolist = fun nil cons -> cons (x, s) nil }
+    type 'a t = 'a iolist
 
-    let (>>=) (m : 'a t) (f : 'a -> 'b t) : 'b t = (); fun s ->
-      let m = m s in
-      { iolist = fun nil cons ->
-        m.iolist nil (fun (x, s) next -> (f x s).iolist next cons) }
+    let return x =
+      { iolist = fun s nil cons -> cons x s nil }
 
-    let (>>) (m : unit t) (f : 'a t) : 'a t = (); fun s ->
-      let m = m s in
-      { iolist = fun nil cons ->
-        m.iolist nil (fun ((), s) next -> (f s).iolist next cons) }
+    let (>>=) m f =
+      { iolist = fun s nil cons ->
+        m.iolist s nil (fun x s next -> (f x).iolist s next cons) }
 
-    let map (f : 'a -> 'b) (m : 'a t) : 'b t = (); fun s ->
-      let m = m s in
-      { iolist = fun nil cons -> m.iolist nil (fun (x, s) next -> cons (f x, s) next) }
+    let (>>) m f =
+      { iolist = fun s nil cons ->
+        m.iolist s nil (fun () s next -> f.iolist s next cons) }
+
+    let map f m =
+      { iolist = fun s nil cons -> m.iolist s nil (fun x s next -> cons (f x) s next) }
 
   end)
 
-  let zero e : 'a t = (); fun s ->
-    { iolist = fun nil cons -> nil e }
+  let zero e =
+    { iolist = fun _ nil cons -> nil e }
 
-  let plus m1 m2 : 'a t = (); fun s ->
-    let m1 = m1 s in
-    { iolist = fun nil cons -> m1.iolist (fun e -> (m2 e s).iolist nil cons) cons }
+  let plus m1 m2 =
+    { iolist = fun s nil cons -> m1.iolist s (fun e -> (m2 e).iolist s nil cons) cons }
 
-  let ignore (m : 'a t) : unit t = (); fun s ->
-    let m = m s in
-    { iolist = fun nil cons -> m.iolist nil (fun (_, s) next -> cons ((), s) next) }
+  let ignore m =
+    { iolist = fun s nil cons -> m.iolist s nil (fun _ s next -> cons () s next) }
 
-  let lift (m : 'a NonLogical.t) : 'a t = (); fun s ->
-    { iolist = fun nil cons -> NonLogical.(m >>= fun x -> cons (x, s) nil) }
+  let lift m =
+    { iolist = fun s nil cons -> NonLogical.(m >>= fun x -> cons x s nil) }
 
   (** State related *)
 
-  let get : P.s t = (); fun s ->
-    { iolist = fun nil cons -> cons (s.sstate, s) nil }
+  let get =
+    { iolist = fun s nil cons -> cons s.sstate s nil }
 
-  let set (sstate : P.s) : unit t = (); fun s ->
-    { iolist = fun nil cons -> cons ((), { s with sstate }) nil }
+  let set (sstate : P.s) =
+    { iolist = fun s nil cons -> cons () { s with sstate } nil }
 
-  let modify (f : P.s -> P.s) : unit t = (); fun s ->
-    { iolist = fun nil cons -> cons ((), { s with sstate = f s.sstate }) nil }
+  let modify (f : P.s -> P.s) =
+    { iolist = fun s nil cons -> cons () { s with sstate = f s.sstate } nil }
 
-  let current : P.e t = (); fun s ->
-    { iolist = fun nil cons -> cons (s.rstate, s) nil }
+  let current =
+    { iolist = fun s nil cons -> cons s.rstate s nil }
 
-  let local (type a) (e:P.e) (m:a t) : a t = (); fun s ->
-    let m = m { s with rstate = e } in
-    { iolist = fun nil cons ->
-      m.iolist nil (fun (x,s') next -> cons (x,{s' with rstate=s.rstate}) next) }
+  let local e m =
+    { iolist = fun s nil cons ->
+      m.iolist { s with rstate = e } nil
+        (fun x s' next -> cons x {s' with rstate = s.rstate} next) }
 
-  let put (w : P.w) : unit t = (); fun s ->
-    { iolist = fun nil cons -> cons ((), { s with wstate = P.wprod s.wstate w }) nil }
+  let put w =
+    { iolist = fun s nil cons -> cons () { s with wstate = P.wprod s.wstate w } nil }
 
-  let update (f : P.u -> P.u) : unit t = (); fun s ->
-    { iolist = fun nil cons -> cons ((), { s with ustate = f s.ustate }) nil }
+  let update (f : P.u -> P.u) =
+    { iolist = fun s nil cons -> cons () { s with ustate = f s.ustate } nil }
 
   (** List observation *)
 
-  let once (m : 'a t) : 'a t = (); fun s ->
-    let m = m s in
-    { iolist = fun nil cons -> m.iolist nil (fun x _ -> cons x nil) }
+  let once m =
+    { iolist = fun s nil cons -> m.iolist s nil (fun x s _ -> cons x s nil) }
 
-  let break (f : rich_exn -> rich_exn option) (m : 'a t) : 'a t = (); fun s ->
-    let m = m s in
-    { iolist = fun nil cons ->
-      m.iolist nil (fun x next -> cons x (fun e -> match f e with None -> next e | Some e -> nil e))
+  let break f m =
+    { iolist = fun s nil cons ->
+      m.iolist s nil (fun x s next -> cons x s (fun e -> match f e with None -> next e | Some e -> nil e))
     }
 
   (** For [reflect] and [split] see the "Backtracking, Interleaving,
       and Terminating Monad Transformers" paper.  *)
   type 'a reified = ('a, rich_exn -> 'a reified) list_view NonLogical.t
 
-  let rec reflect (m : 'a reified) : 'a iolist =
-    { iolist = fun nil cons ->
+  let rec reflect (m : ('a * state) reified) : 'a iolist =
+    { iolist = fun s0 nil cons ->
       let next = function
       | Nil e -> nil e
-      | Cons (x, l) -> cons x (fun e -> (reflect (l e)).iolist nil cons)
+      | Cons ((x, s), l) -> cons x s (fun e -> (reflect (l e)).iolist s0 nil cons)
       in
       NonLogical.(m >>= next)
     }
 
-  let split (m : 'a t) : ('a, rich_exn -> 'a t) list_view t = (); fun s ->
-    let m = m s in
+  let split m : ('a, rich_exn -> 'a t) list_view t =
     let rnil e = NonLogical.return (Nil e) in
-    let rcons p l = NonLogical.return (Cons (p, l)) in
-    { iolist = fun nil cons ->
+    let rcons p s l = NonLogical.return (Cons ((p, s), l)) in
+    { iolist = fun s nil cons ->
       let open NonLogical in
-      m.iolist rnil rcons >>= begin function
-      | Nil e -> cons (Nil e, s) nil
+      m.iolist s rnil rcons >>= begin function
+      | Nil e -> cons (Nil e) s nil
       | Cons ((x, s), l) ->
-        let l e = (); fun _ -> reflect (l e) in
-        cons (Cons (x, l), s) nil
+        let l e = reflect (l e) in
+        cons (Cons (x, l)) s nil
       end }
 
   let run m r s =
     let s = { wstate = P.wunit; ustate = P.uunit; rstate = r; sstate = s } in
-    let m = m s in
     let rnil e = NonLogical.return (Nil e) in
-    let rcons (x, s) l =
+    let rcons x s l =
       let p = (x, s.sstate, s.wstate, s.ustate) in
       NonLogical.return (Cons (p, l))
     in
-    m.iolist rnil rcons
+    m.iolist s rnil rcons
 
   let repr x = x
 
-- 
cgit v1.2.3


From b846c413c2e79520a5238c5a0775f5cd73d61bac Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 18 Apr 2015 10:16:44 +0200
Subject: Inlining "fun" and "forall" tokens in parser, so that alternative
 notations for them (e.g. "fun ... ⇒ ...") factor well (see #2268).

---
 parsing/g_constr.ml4 | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 3bb029a888..74f17f9fb6 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -223,12 +223,6 @@ GEXTEND Gram
           CHole (!@loc, None, IntroAnonymous, Some arg)
       ] ]
   ;
-  forall:
-    [ [ "forall" -> () ] ]
-  ;
-  lambda:
-    [ [ "fun" -> () ] ]
-  ;
   record_declaration:
     [ [ fs = LIST0 record_field_declaration SEP ";" -> CRecord (!@loc, None, fs)
 (*       | c = lconstr; "with"; fs = LIST1 record_field_declaration SEP ";" -> *)
@@ -240,9 +234,9 @@ GEXTEND Gram
       (id, abstract_constr_expr c (binders_of_lidents params)) ] ]
   ;
   binder_constr:
-    [ [ forall; bl = open_binders; ","; c = operconstr LEVEL "200" ->
+    [ [ "forall"; bl = open_binders; ","; c = operconstr LEVEL "200" ->
           mkCProdN (!@loc) bl c
-      | lambda; bl = open_binders; "=>"; c = operconstr LEVEL "200" ->
+      | "fun"; bl = open_binders; "=>"; c = operconstr LEVEL "200" ->
           mkCLambdaN (!@loc) bl c
       | "let"; id=name; bl = binders; ty = type_cstr; ":=";
         c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
-- 
cgit v1.2.3


From 94afd8996251c30d2188a75934487009538e1303 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 20 Apr 2015 12:44:25 +0200
Subject: Change magic numbers.

---
 configure.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/configure.ml b/configure.ml
index bbe4352080..92d71813c1 100644
--- a/configure.ml
+++ b/configure.ml
@@ -14,8 +14,8 @@ open Printf
 let coq_version = "8.5beta2"
 let coq_macos_version = "8.4.92" (** "[...] should be a string comprised of
 three non-negative, period-separed integers [...]" *)
-let vo_magic = 8591
-let state_magic = 58501
+let vo_magic = 8492
+let state_magic = 58502
 let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqmktop";"coqworkmgr";
 "coqdoc";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert";"coqdep"]
 
-- 
cgit v1.2.3


From a33f7ad548ed312a2665c87baca9fb7b233e8cbf Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 20 Apr 2015 16:20:40 +0200
Subject: Remove spurious ".v" from warning message.

---
 tools/coqdep_common.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 2e6a15cebd..d86e05d8cf 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -136,10 +136,8 @@ let error_cannot_parse s (i,j) =
   exit 1
 
 let warning_module_notfound f s =
-  eprintf "*** Warning: in file %s, library " f;
-  eprintf "%s.v is required and has not been found in the loadpath!\n"
-    (String.concat "." s);
-  flush stderr
+  eprintf "*** Warning: in file %s, library %s is required and has not been found in the loadpath!\n%!"
+    f (String.concat "." s)
 
 let warning_notfound f s =
   eprintf "*** Warning: in file %s, the file " f;
-- 
cgit v1.2.3


From ce6bbd05b7d741750228956a7e045cb202ec0e74 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 2 Apr 2015 18:41:09 +0200
Subject: Some dead code.

---
 pretyping/evarconv.ml | 7 -------
 1 file changed, 7 deletions(-)

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f388f90057..97b1b16455 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -201,13 +201,6 @@ let ise_and evd l =
 	| UnifFailure _ as x -> x in
   ise_and evd l
 
-(* This function requires to get the outermost arguments first.  It is
-   a fold_right for backward compatibility.
-
-   It tries to unify the suffix of 2 lists element by element and if
-   it reaches the end of a list, it returns the remaining elements in
-   the other list if there are some.
-*)
 let ise_exact ise x1 x2 =
   match ise x1 x2 with
   | None, out -> out
-- 
cgit v1.2.3


From 7d261ef454e918c70b8fff1dd10bbe0fbdcb57a8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 21 Apr 2015 15:54:26 +0200
Subject: Fixing #3376 and #4191 (wrong index of maximally-inserted implicit
 argument in the presence of let-ins).

---
 interp/constrintern.ml        | 2 +-
 test-suite/bugs/closed/4191.v | 5 +++++
 2 files changed, 6 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/4191.v

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 5151d2a10a..8f0d56c5bd 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1913,7 +1913,7 @@ let interp_rawcontext_evars env evdref bl =
 	  | Some b ->
 	      let c = understand_judgment_tcc env evdref b in
 	      let d = (na, Some c.uj_val, c.uj_type) in
-		(push_rel d env, d::params, succ n, impls))
+		(push_rel d env, d::params, n, impls))
       (env,[],1,[]) (List.rev bl)
   in (env, par), impls
 
diff --git a/test-suite/bugs/closed/4191.v b/test-suite/bugs/closed/4191.v
new file mode 100644
index 0000000000..290bb384d9
--- /dev/null
+++ b/test-suite/bugs/closed/4191.v
@@ -0,0 +1,5 @@
+(* Test maximal implicit arguments in the presence of let-ins *)
+Definition foo (x := 1) {y : nat} (H : y = y) : True := I.
+Definition bar {y : nat} (x := 1) (H : y = y) : True := I.
+Check bar (eq_refl 1).
+Check foo (eq_refl 1). 
-- 
cgit v1.2.3


From 9fa7f38b74ec26f880d9ec983a5a1c8699e0a612 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 21 Apr 2015 16:35:15 +0200
Subject: Fixing #3383 (a "return" clause without an "in" clause is not enough
 for being able to interpret a "match" as a constr pattern).

---
 pretyping/patternops.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 705e594af1..a766b1265e 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -395,7 +395,9 @@ let rec pat_of_raw metas vars = function
 	| Some p, Some (_,_,nal) ->
           let nvars = na :: List.rev nal @ vars in
           rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p))
-	| _ -> PMeta None
+        | (None | Some (GHole _)), None -> PMeta None
+	| Some p, None ->
+            user_err_loc (loc,"",strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.")
       in
       let info =
 	{ cip_style = sty;
-- 
cgit v1.2.3


From a45bd5981092cceefc4d4d30f9be327bb69c22d8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 21 Apr 2015 16:36:31 +0200
Subject: Fixing #4198 (looking for subterms also in the return clause of
 match).

This is actually not so perfect because of the lambdas in the return
clause which we would not like to look in.
---
 dev/base_include             | 1 +
 pretyping/constr_matching.ml | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/dev/base_include b/dev/base_include
index de63c557d3..d58b6ad13c 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -86,6 +86,7 @@ open Cbv
 open Classops
 open Clenv
 open Clenvtac
+open Constr_matching
 open Glob_term
 open Glob_ops
 open Coercion
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 161cffa865..e281807131 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -428,7 +428,7 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
       | [] -> assert false
       | c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc))
       in
-      let sub = (env, c1) :: subargs env lc in
+      let sub = (env, hd) :: (env, c1) :: subargs env lc in
       let next () = try_aux sub next_mk_ctx next in
       authorized_occ env sigma partial_app closed pat c mk_ctx next
   | Fix (indx,(names,types,bodies)) ->
-- 
cgit v1.2.3


From 2a5fd12d597d4337810ae367ea3a49720ee3d80c Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 21 Apr 2015 17:43:01 +0200
Subject: STM: print trace on "anomaly, no safe id attached"

---
 lib/errors.ml  | 2 ++
 lib/errors.mli | 1 +
 stm/stm.ml     | 2 +-
 3 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/lib/errors.ml b/lib/errors.ml
index a4ec357ee4..13f3916477 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -99,6 +99,8 @@ let iprint (e, info) = print ~info e
 (** Same as [print], except that the "Please report" part of an anomaly
     isn't printed (used in Ltac debugging). *)
 let print_no_report e = print_gen (print_anomaly false) !handle_stack e
+let iprint_no_report (e, info) =
+  print_gen (print_anomaly false) !handle_stack e ++ print_backtrace info
 
 (** Predefined handlers **)
 
diff --git a/lib/errors.mli b/lib/errors.mli
index 03caa6a9f8..5bd5724746 100644
--- a/lib/errors.mli
+++ b/lib/errors.mli
@@ -80,6 +80,7 @@ val iprint : Exninfo.iexn -> Pp.std_ppcmds
 (** Same as [print], except that the "Please report" part of an anomaly
     isn't printed (used in Ltac debugging). *)
 val print_no_report : exn -> Pp.std_ppcmds
+val iprint_no_report : Exninfo.iexn -> Pp.std_ppcmds
 
 (** Critical exceptions should not be caught and ignored by mistake
     by inner functions during a [vernacinterp]. They should be handled
diff --git a/stm/stm.ml b/stm/stm.ml
index 38745e2273..f36b757f29 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2018,7 +2018,7 @@ let handle_failure (e, info) vcs tty =
       end;
       VCS.print ();
       anomaly(str"error with no safe_id attached:" ++ spc() ++
-        Errors.print_no_report e)
+        Errors.iprint_no_report (e, info))
   | Some (safe_id, id) ->
       prerr_endline ("Failed at state " ^ Stateid.to_string id);
       VCS.restore vcs;
-- 
cgit v1.2.3


From a201b73607d0094c89776ea4b51483bf3d1f9cec Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 22 Apr 2015 08:10:20 +0200
Subject: Remove some spurious spaces in generated Makefiles.

---
 tools/coq_makefile.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 0931fd5506..00088570b3 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -299,7 +299,7 @@ let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) in
       printf "find %s/%s -maxdepth 0 -and -empty -exec rmdir -p \\{\\} \\;\\n' >> \"$@\"\n" dir kind
     in
     printf "uninstall_me.sh: %s\n" !makefile_name;
-    print "\techo '#!/bin/sh' > $@ \n";
+    print "\techo '#!/bin/sh' > $@\n";
     if (not_empty cmxsfiles) then uninstall_by_root where_what_cmxs;
     uninstall_by_root where_what_oth;
     if not_empty vfiles then uninstall_one_kind "html" doc_dir;
@@ -496,7 +496,7 @@ endif\n";
           print "\n"
 
 let parameters () =
-  print ".DEFAULT_GOAL := all\n\n# \n";
+  print ".DEFAULT_GOAL := all\n\n";
   print "# This Makefile may take arguments passed as environment variables:\n";
   print "# COQBIN to specify the directory where Coq binaries resides;\n";
   print "# TIMECMD set a command to log .v compilation time;\n";
-- 
cgit v1.2.3


From 98a710caf5e907344329ee9e9f7b5fd87c50836f Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 22 Apr 2015 09:15:39 +0200
Subject: Do not use list concatenation when gluing streams together, just mark
 them as glued.

Possible improvement: rotate using the left children in the glue function,
so that the iter function becomes mostly tail-recursive. Drawback: two
allocations per glue instead of a single one.

This commit makes the following command go from 7.9s to 3.0s:

coqtop <<< "Require Import BigZ ZBinary Reals OrdersEx. Time SearchPattern _." | tail -n 1
---
 lib/pp.ml | 29 ++++++++++++++++++++++-------
 1 file changed, 22 insertions(+), 7 deletions(-)

diff --git a/lib/pp.ml b/lib/pp.ml
index 76046a7f91..e8b42ed797 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -26,15 +26,30 @@ module Glue : sig
 
 end = struct
 
-  type 'a t = 'a list
+  type 'a t = GEmpty | GLeaf of 'a | GNode of 'a t * 'a t
 
-  let atom x = [x]
-  let glue x y = y @ x
-  let empty = []
-  let is_empty x = x = []
+  let atom x = GLeaf x
+
+  let glue x y =
+    match x, y with
+    | GEmpty, _ -> y
+    | _, GEmpty -> x
+    | _, _ -> GNode (x,y)
+
+  let empty = GEmpty
+
+  let is_empty x = x = GEmpty
+
+  let rec iter f = function
+    | GEmpty -> ()
+    | GLeaf x -> f x
+    | GNode (x,y) -> iter f x; iter f y
+
+  let rec map f = function
+    | GEmpty -> GEmpty
+    | GLeaf x -> GLeaf (f x)
+    | GNode (x,y) -> GNode (map f x, map f y)
 
-  let iter f g = List.iter f (List.rev g)
-  let map = List.map
 end
 
 module Tag :
-- 
cgit v1.2.3


From 18eae5be263a8b329ffa73d350faf3193fa4097a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 22 Apr 2015 14:44:17 +0200
Subject: Update CHANGES

---
 CHANGES | 40 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)

diff --git a/CHANGES b/CHANGES
index 57bb9f1996..b02467a462 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,43 @@
+Changes from V8.5beta1 to V8.5beta2
+===================================
+
+Logic
+
+- The VM now supports inductive types with more than 200 non-constant
+  constructors.
+
+Tactics
+
+- A script using the admit tactic can no longer be concluded by either
+  Qed or Defined. In the first case, Admitted can be used instead. In
+  the second case, a subproof should be used.
+
+- The easy tactic and the now tactical now have a more predictable
+  behavior, but they might now discharge some previously unsolved goals.
+
+Extraction
+
+- Definitions extracted to Haskell GHC should no longer randomly
+  segfault when some Coq types cannot be represented by Haskell types.
+
+- Definitions can now be extracted to Json for post-processing.
+
+Tools
+
+- Option -I -as has been removed, and option -R -as has been
+  deprecated. In both cases, option -R can be used instead.
+
+- coq_makefile now generates double-colon rules for rules such as clean.
+
+API
+
+- The interface of [change] has changed to take a [change_arg], which
+  can be built from a [constr] using [make_change_arg].
+
+- [pattern_of_constr] now returns a triplet including the cleaned-up
+  [evar_map], removing the evars that were turned into metas.
+
+
 Changes from V8.4 to V8.5beta1
 ==============================
 
-- 
cgit v1.2.3


From 8e5ecc6a3e334620ff6149706008fe4432567870 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 22 Apr 2015 15:37:59 +0200
Subject: More precise numbers about Benjamin's fix for the VM.

---
 CHANGES | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/CHANGES b/CHANGES
index b02467a462..b1dffde147 100644
--- a/CHANGES
+++ b/CHANGES
@@ -3,8 +3,8 @@ Changes from V8.5beta1 to V8.5beta2
 
 Logic
 
-- The VM now supports inductive types with more than 200 non-constant
-  constructors.
+- The VM now supports inductive types with up to 8388851 non-constant
+  constructors and up to 8388607 constant ones.
 
 Tactics
 
-- 
cgit v1.2.3


From 3d2cf9fea0aec4ae839f70acd896958772b4caaf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 21 Apr 2015 17:12:29 +0200
Subject: Test for #4198 (appcontext in return clause of match).

---
 test-suite/bugs/closed/4198.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 test-suite/bugs/closed/4198.v

diff --git a/test-suite/bugs/closed/4198.v b/test-suite/bugs/closed/4198.v
new file mode 100644
index 0000000000..ef991365d5
--- /dev/null
+++ b/test-suite/bugs/closed/4198.v
@@ -0,0 +1,13 @@
+Require Import List.
+Open Scope list_scope.
+Goal forall A (x x' : A) (xs xs' : list A) (H : x::xs = x'::xs'),
+       let k :=
+           (match H in (_ = y) return x = hd x y with
+              | eq_refl => eq_refl
+            end : x = x')
+       in k = k.
+  simpl.
+  intros.
+  match goal with
+    | [ |- appcontext G[@hd] ] => idtac
+  end.
-- 
cgit v1.2.3


From db294322a9ae8954d5325ad0f02e37bf0db70548 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 22 Apr 2015 18:50:05 +0200
Subject: Fixing non exhaustive pattern-matching.

---
 pretyping/patternops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index a766b1265e..fb629d049f 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -395,7 +395,7 @@ let rec pat_of_raw metas vars = function
 	| Some p, Some (_,_,nal) ->
           let nvars = na :: List.rev nal @ vars in
           rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p))
-        | (None | Some (GHole _)), None -> PMeta None
+        | (None | Some (GHole _)), _ -> PMeta None
 	| Some p, None ->
             user_err_loc (loc,"",strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.")
       in
-- 
cgit v1.2.3


From b4552eb74c7ee577339b44924b59c2ab25f893d2 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 22 Apr 2015 13:29:46 +0200
Subject: Declarative mode: remaining goals are "given up" when closing blocks.

Restores the intended behaviour from v8.3 and earlier.---
 plugins/decl_mode/decl_proof_instr.ml | 30 +++++++++++++++++++++++++++---
 1 file changed, 27 insertions(+), 3 deletions(-)

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 9d0b7f3466..36273faae2 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -125,10 +125,34 @@ let go_to_proof_mode () =
 
 (* closing gaps *)
 
+(* spiwack: should use [Proofview.give_up] but that would require
+   moving the whole declarative mode into the new proof engine.  It
+   will eventually have to be done.
+
+   As far as I can tell, [daimon_tac] is used after a [thus thesis],
+   it will leave uninstantiated variables instead of giving a relevant
+   message at [Qed]. *)
 let daimon_tac gls =
   set_daimon_flag ();
   {it=[];sigma=sig_sig gls;}
 
+let daimon_instr env p =
+  let (p,(status,_)) =
+    Proof.run_tactic env begin
+      Proofview.tclINDEPENDENT Proofview.give_up
+    end p
+  in
+  p,status
+
+let do_daimon () =
+  let env = Global.env () in
+  let status =
+    Proof_global.with_current_proof begin fun _ p ->
+      daimon_instr env p
+    end
+  in
+  if not status then Pp.feedback Feedback.AddedAxiom else ()
+
 (* post-instruction focus management *)
 
 let goto_current_focus () = 
@@ -144,7 +168,7 @@ let goto_current_focus_or_top () =
 (* return *)
 
 let close_tactic_mode () =
-  try goto_current_focus ()
+  try do_daimon ();goto_current_focus ()
   with Not_found ->
     error "\"return\" cannot be used outside of Declarative Proof Mode."
 
@@ -165,7 +189,7 @@ let close_block bt pts =
       in
       match bt,stack with
 	B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] ->
-	  (goto_current_focus ())
+	  do_daimon ();goto_current_focus ()
       | _, Claim::_ ->
 	  error "\"end claim\" expected."
       | _, Focus_claim::_ ->
@@ -196,7 +220,7 @@ let close_previous_case pts =
     match get_stack pts with
 	Per (et,_,_,_) :: _ -> ()
       | Suppose_case :: Per (et,_,_,_) :: _ ->
-	  goto_current_focus ()
+	  do_daimon ();goto_current_focus ()
       | _ -> error "Not inside a proof per cases or induction."
 
 (* Proof instructions *)
-- 
cgit v1.2.3


From 74d7dd7ae08dedfd80c056a345c1b3398eb91b5e Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 22 Apr 2015 17:39:42 +0200
Subject: Pp: obsolete comment.

Was made incorrect by 98a710caf5e907344329ee9e9f7b5fd87c50836f .---
 lib/pp.ml | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/lib/pp.ml b/lib/pp.ml
index e8b42ed797..6e6b32c590 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -8,13 +8,9 @@
 
 module Glue : sig
 
-  (* A left associative glue implements efficient glue operator
-     when used as left associative.  If glue is denoted ++ then
+  (** The [Glue] module implements a container data structure with
+      efficient concatenation. *)
 
-        a ++ b ++ c ++ d = ((a ++ b) ++ c) ++ d = [d] @ ([c] @ ([b] @  [a]))
-
-     I.e. if the short list is the second argument
-  *)
   type 'a t
 
   val atom : 'a -> 'a t
-- 
cgit v1.2.3


From 501d6dd5691474c807a722d9b5b6e3fa9d83c749 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 22 Apr 2015 18:51:48 +0200
Subject: Tactical `progress` compares term up to potentially equalisable
 universes.

Followup of: f7b29094fe7cc13ea475447bd30d9a8b942f0fef . In particular, re-closes #3593.

As a side effect, fixes an undiscovered bug of the `eq_constr` tactic which didn't consider terms up to evar instantiation.---
 kernel/constr.ml              | 54 +++++++++++++++++------------------
 kernel/constr.mli             | 20 +++++++------
 library/universes.ml          | 66 ++++++++++++++++++++++++++++++-------------
 library/universes.mli         |  8 ++++++
 pretyping/evarutil.ml         | 21 +++++++++++++-
 pretyping/evarutil.mli        |  7 +++++
 pretyping/evd.ml              |  3 --
 pretyping/evd.mli             |  4 ---
 proofs/proofview.ml           | 14 +--------
 tactics/extratactics.ml4      |  2 +-
 test-suite/bugs/closed/3593.v | 10 +++++++
 test-suite/bugs/opened/3593.v | 10 -------
 12 files changed, 131 insertions(+), 88 deletions(-)
 create mode 100644 test-suite/bugs/closed/3593.v
 delete mode 100644 test-suite/bugs/opened/3593.v

diff --git a/kernel/constr.ml b/kernel/constr.ml
index e823c01b17..e2b1d3fd9c 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -475,7 +475,7 @@ let map_with_binders g f l c0 = match kind c0 with
    optimisation that physically equal arrays are equals (hence the
    calls to {!Array.equal_norefl}). *)
 
-let compare_head_gen_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 =
+let compare_head_gen_leq_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 =
   match kind1 t1, kind2 t2 with
   | Rel n1, Rel n2 -> Int.equal n1 n2
   | Meta m1, Meta m2 -> Int.equal m1 m2
@@ -512,13 +512,19 @@ let compare_head_gen_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 =
    not taken into account *)
 
 let compare_head_gen_leq eq_universes leq_sorts eq leq t1 t2 =
-  compare_head_gen_with kind kind  eq_universes leq_sorts eq leq t1 t2
+  compare_head_gen_leq_with kind kind  eq_universes leq_sorts eq leq t1 t2
 
-(* [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to compare
-   the immediate subterms of [c1] of [c2] if needed, [u] to compare universe
-   instances and [s] to compare sorts; Cast's,
+(* [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to
+   compare the immediate subterms of [c1] of [c2] if needed, [u] to
+   compare universe instances and [s] to compare sorts; Cast's,
    application associativity, binders name and Cases annotations are
-   not taken into account *)
+   not taken into account.
+
+   [compare_head_gen_with] is a variant taking kind-of-term functions,
+   to expose subterms of [c1] and [c2], as arguments. *)
+
+let compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq t1 t2 =
+  compare_head_gen_leq_with kind1 kind2 eq_universes eq_sorts eq eq t1 t2
 
 let compare_head_gen eq_universes eq_sorts eq t1 t2 =
   compare_head_gen_leq eq_universes eq_sorts eq eq t1 t2
@@ -536,14 +542,6 @@ let rec eq_constr m n =
 
 let equal m n = eq_constr m n (* to avoid tracing a recursive fun *)
 
-let rec equal_with kind1 kind2 m n =
-  (* note that pointer equality is not sufficient to ensure equality
-     up to [eq_evars], because we may evaluates evars of [m] and [n]
-     in different evar contexts. *)
-  let req_constr m n = equal_with kind1 kind2 m n in
-  compare_head_gen_with kind1 kind2
-    (fun _ -> Instance.equal) Sorts.equal req_constr req_constr m n
-
 let eq_constr_univs univs m n =
   if m == n then true
   else 
@@ -567,7 +565,7 @@ let leq_constr_univs univs m n =
     let rec compare_leq m n =
       compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n
     and leq_constr' m n = m == n || compare_leq m n in
-      compare_leq m n
+    compare_leq m n
 
 let eq_constr_univs_infer univs m n =
   if m == n then true, Constraint.empty
@@ -578,16 +576,16 @@ let eq_constr_univs_infer univs m n =
       if Sorts.equal s1 s2 then true
       else
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	  if Univ.check_eq univs u1 u2 then true
-	  else
-	    (cstrs := Univ.enforce_eq u1 u2 !cstrs;
-	     true)
+	if Univ.check_eq univs u1 u2 then true
+	else
+	  (cstrs := Univ.enforce_eq u1 u2 !cstrs;
+	   true)
     in
     let rec eq_constr' m n = 
       m == n ||	compare_head_gen eq_universes eq_sorts eq_constr' m n
     in
     let res = compare_head_gen eq_universes eq_sorts eq_constr' m n in
-      res, !cstrs
+    res, !cstrs
 
 let leq_constr_univs_infer univs m n =
   if m == n then true, Constraint.empty
@@ -598,18 +596,18 @@ let leq_constr_univs_infer univs m n =
       if Sorts.equal s1 s2 then true
       else
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	  if Univ.check_eq univs u1 u2 then true
-	  else (cstrs := Univ.enforce_eq u1 u2 !cstrs;
-		true)
+	if Univ.check_eq univs u1 u2 then true
+	else (cstrs := Univ.enforce_eq u1 u2 !cstrs;
+	      true)
     in
     let leq_sorts s1 s2 = 
       if Sorts.equal s1 s2 then true
       else 
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	  if Univ.check_leq univs u1 u2 then true
-	  else
-	    (cstrs := Univ.enforce_leq u1 u2 !cstrs; 
-	     true)
+	if Univ.check_leq univs u1 u2 then true
+	else
+	  (cstrs := Univ.enforce_leq u1 u2 !cstrs; 
+	   true)
     in
     let rec eq_constr' m n = 
       m == n ||	compare_head_gen eq_universes eq_sorts eq_constr' m n
@@ -618,7 +616,7 @@ let leq_constr_univs_infer univs m n =
       compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n
     and leq_constr' m n = m == n || compare_leq m n in
     let res = compare_leq m n in
-      res, !cstrs
+    res, !cstrs
 
 let always_true _ _ = true
 
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 67d1adedf6..e6a3e71f89 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -203,14 +203,6 @@ val kind : constr -> (constr, types) kind_of_term
    and application grouping *)
 val equal : constr -> constr -> bool
 
-(** [equal_with_evars k1 k2 a b] is true when [a] equals [b] modulo
-    alpha, casts, application grouping, and using [k1] to expose the
-    head of [a] and [k2] to expose the head of [b]. *)
-val equal_with :
-  (constr -> (constr,types) kind_of_term) ->
-  (constr -> (constr,types) kind_of_term) ->
-  constr -> constr -> bool
-
 (** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts,
    application grouping and the universe equalities in [u]. *)
 val eq_constr_univs : constr Univ.check_function
@@ -293,6 +285,18 @@ val compare_head_gen : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
   (constr -> constr -> bool) ->
   constr -> constr -> bool
 
+(** [compare_head_gen_with k1 k2 u s f c1 c2] compares [c1] and [c2]
+    like [compare_head_gen u s f c1 c2], except that [k1] (resp. [k2])
+    is used,rather than {!kind}, to expose the immediate subterms of
+    [c1] (resp. [c2]). *)
+val compare_head_gen_with :
+  (constr -> (constr,types) kind_of_term) ->
+  (constr -> (constr,types) kind_of_term) ->
+  (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
+  (Sorts.t -> Sorts.t -> bool) ->
+  (constr -> constr -> bool) ->
+  constr -> constr -> bool
+
 (** [compare_head_gen_leq u s f fle c1 c2] compare [c1] and [c2] using
     [f] to compare the immediate subterms of [c1] of [c2] for
     conversion, [fle] for cumulativity, [u] to compare universe
diff --git a/library/universes.ml b/library/universes.ml
index 9fddc7067b..3a8ee26254 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -139,6 +139,32 @@ let eq_constr_univs_infer univs m n =
     let res = Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in
       res, !cstrs
 
+(** Variant of [eq_constr_univs_infer] taking kind-of-term functions,
+    to expose subterms of [m] and [n], arguments. *)
+let eq_constr_univs_infer_with kind1 kind2 univs m n =
+  (* spiwack: duplicates the code of [eq_constr_univs_infer] because I
+     haven't find a way to factor the code without destroying
+     pointer-equality optimisations in [eq_constr_univs_infer].
+     Pointer equality is not sufficient to ensure equality up to
+     [kind1,kind2], because [kind1] and [kind2] may be different,
+     typically evaluating [m] and [n] in different evar maps. *)
+  let cstrs = ref Constraints.empty in
+  let eq_universes strict = Univ.Instance.check_eq univs in
+  let eq_sorts s1 s2 = 
+    if Sorts.equal s1 s2 then true
+    else
+      let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
+      if Univ.check_eq univs u1 u2 then true
+      else
+	(cstrs := Constraints.add (u1, UEq, u2) !cstrs;
+	 true)
+  in
+  let rec eq_constr' m n = 
+    Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n
+  in
+  let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n in
+  res, !cstrs
+
 let leq_constr_univs_infer univs m n =
   if m == n then true, Constraints.empty
   else 
@@ -148,18 +174,18 @@ let leq_constr_univs_infer univs m n =
       if Sorts.equal s1 s2 then true
       else
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	  if Univ.check_eq univs u1 u2 then true
-	  else (cstrs := Constraints.add (u1, UEq, u2) !cstrs;
-		true)
+	if Univ.check_eq univs u1 u2 then true
+	else (cstrs := Constraints.add (u1, UEq, u2) !cstrs;
+	      true)
     in
     let leq_sorts s1 s2 = 
       if Sorts.equal s1 s2 then true
       else 
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	  if Univ.check_leq univs u1 u2 then true
-	  else
-	    (cstrs := Constraints.add (u1, ULe, u2) !cstrs; 
-	     true)
+	if Univ.check_leq univs u1 u2 then true
+	else
+	  (cstrs := Constraints.add (u1, ULe, u2) !cstrs; 
+	   true)
     in
     let rec eq_constr' m n = 
       m == n ||	Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
@@ -169,7 +195,7 @@ let leq_constr_univs_infer univs m n =
 	eq_constr' leq_constr' m n
     and leq_constr' m n = m == n || compare_leq m n in
     let res = compare_leq m n in
-      res, !cstrs
+    res, !cstrs
 
 let eq_constr_universes m n =
   if m == n then true, Constraints.empty
@@ -188,7 +214,7 @@ let eq_constr_universes m n =
       m == n ||	Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
     in
     let res = Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in
-      res, !cstrs
+    res, !cstrs
 
 let leq_constr_universes m n =
   if m == n then true, Constraints.empty
@@ -216,22 +242,22 @@ let leq_constr_universes m n =
       Constr.compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n
     and leq_constr' m n = m == n || compare_leq m n in
     let res = compare_leq m n in
-      res, !cstrs
+    res, !cstrs
 
 let compare_head_gen_proj env equ eqs eqc' m n =
   match kind_of_term m, kind_of_term n with
   | Proj (p, c), App (f, args)
   | App (f, args), Proj (p, c) -> 
-    (match kind_of_term f with
-    | Const (p', u) when eq_constant (Projection.constant p) p' -> 
-      let pb = Environ.lookup_projection p env in
-      let npars = pb.Declarations.proj_npars in
-	if Array.length args == npars + 1 then
-	  eqc' c args.(npars)
-	else false
-    | _ -> false)
+      (match kind_of_term f with
+      | Const (p', u) when eq_constant (Projection.constant p) p' -> 
+          let pb = Environ.lookup_projection p env in
+          let npars = pb.Declarations.proj_npars in
+	  if Array.length args == npars + 1 then
+	    eqc' c args.(npars)
+	  else false
+      | _ -> false)
   | _ -> Constr.compare_head_gen equ eqs eqc' m n
-    
+      
 let eq_constr_universes_proj env m n =
   if m == n then true, Constraints.empty
   else 
@@ -249,7 +275,7 @@ let eq_constr_universes_proj env m n =
       m == n ||	compare_head_gen_proj env eq_universes eq_sorts eq_constr' m n
     in
     let res = eq_constr' m n in
-      res, !cstrs
+    res, !cstrs
 
 (* Generator of levels *)
 let new_univ_level, set_remote_new_univ_level =
diff --git a/library/universes.mli b/library/universes.mli
index 252648d7dc..5527da0903 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -66,6 +66,14 @@ val to_constraints : universes -> universe_constraints -> constraints
    application grouping, the universe constraints in [u] and additional constraints [c]. *)
 val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained
 
+(** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of
+    {!eq_constr_univs_infer} taking kind-of-term functions, to expose
+    subterms of [m] and [n], arguments. *)
+val eq_constr_univs_infer_with :
+  (constr -> (constr,types) kind_of_term) ->
+  (constr -> (constr,types) kind_of_term) ->
+  Univ.universes -> constr -> constr -> bool universe_constrained
+
 (** [leq_constr_univs u a b] is [true, c] if [a] is convertible to [b]
     modulo alpha, casts, application grouping, the universe constraints
     in [u] and additional constraints [c]. *)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 201a16ebeb..2508f4ef3b 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -844,6 +844,25 @@ let subterm_source evk (loc,k) =
   (loc,Evar_kinds.SubEvar evk)
 
 
-(** Term exploration up to isntantiation. *)
+(** Term exploration up to instantiation. *)
 let kind_of_term_upto sigma t =
   Constr.kind (Reductionops.whd_evar sigma t)
+
+(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
+    [u] up to existential variable instantiation and equalisable
+    universes. The term [t] is interpreted in [sigma1] while [u] is
+    interpreted in [sigma2]. The universe constraints in [sigma2] are
+    assumed to be an extention of those in [sigma1]. *)
+let eq_constr_univs_test sigma1 sigma2 t u =
+  (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *)
+  let open Evd in
+  let b, c =
+    Universes.eq_constr_univs_infer_with
+      (fun t -> kind_of_term_upto sigma1 t)
+      (fun u -> kind_of_term_upto sigma2 u)
+      (universes sigma2) t u
+  in
+  if b then
+    try let _ = add_universe_constraints sigma2 c in true
+    with Univ.UniverseInconsistency _ | UniversesDiffer -> false
+  else false
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 49036798e6..f1d94b0a4f 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -206,6 +206,13 @@ val flush_and_check_evars :  evar_map -> constr -> constr
     value of [e] in [sigma] is (recursively) used. *)
 val kind_of_term_upto : evar_map -> constr -> (constr,types) kind_of_term
 
+(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
+    [u] up to existential variable instantiation and equalisable
+    universes. The term [t] is interpreted in [sigma1] while [u] is
+    interpreted in [sigma2]. The universe constraints in [sigma2] are
+    assumed to be an extention of those in [sigma1]. *)
+val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool
+
 (** {6 debug pretty-printer:} *)
 
 val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index bf519fb7c0..f414d71dc1 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1304,9 +1304,6 @@ let e_eq_constr_univs evdref t u =
   let evd, b = eq_constr_univs !evdref t u in
     evdref := evd; b
 
-let eq_constr_univs_test evd t u =
-  snd (eq_constr_univs evd t u)
-
 (**********************************************************)
 (* Accessing metas *)
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index fe785a8314..eca6d60ad5 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -562,10 +562,6 @@ val eq_constr_univs : evar_map -> constr -> constr -> evar_map * bool
 val e_eq_constr_univs : evar_map ref -> constr -> constr -> bool
 (** Syntactic equality up to universes. *)
 
-val eq_constr_univs_test : evar_map -> constr -> constr -> bool
-(** Syntactic equality up to universes, throwing away the (consistent) constraints
-    in case of success. *)
-
 (********************************************************************)
 (* constr with holes and pending resolution of classes, conversion  *)
 (* problems, candidates, etc.                                       *)
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 6f62634133..6e653806b7 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -722,19 +722,7 @@ let give_up =
 
 module Progress = struct
 
-  (** equality function up to evar instantiation in heterogeneous
-      contexts. *)
-  (* spiwack (2015-02-19): In the previous version of progress an
-     equality which considers two universes equal when it is consistent
-     tu unify them ([Evd.eq_constr_univs_test]) was used. Maybe this
-     behaviour has to be restored as well. This has to be established by
-     practice. *)
-    
-  let rec eq_constr sigma1 sigma2 t1 t2 =
-    Constr.equal_with
-      (fun t -> Evarutil.kind_of_term_upto sigma1 t)
-      (fun t -> Evarutil.kind_of_term_upto sigma2 t)
-      t1 t2
+  let eq_constr = Evarutil.eq_constr_univs_test
 
   (** equality function on hypothesis contexts *)
   let eq_named_context_val sigma1 sigma2 ctx1 ctx2 =
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 891e2dba51..7f0a4c6609 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -772,7 +772,7 @@ END
 let eq_constr x y = 
   Proofview.Goal.enter (fun gl ->
     let evd = Proofview.Goal.sigma gl in
-      if Evd.eq_constr_univs_test evd x y then Proofview.tclUNIT () 
+      if Evarutil.eq_constr_univs_test evd evd x y then Proofview.tclUNIT () 
       else Tacticals.New.tclFAIL 0 (str "Not equal"))
 
 TACTIC EXTEND constr_eq
diff --git a/test-suite/bugs/closed/3593.v b/test-suite/bugs/closed/3593.v
new file mode 100644
index 0000000000..378db68570
--- /dev/null
+++ b/test-suite/bugs/closed/3593.v
@@ -0,0 +1,10 @@
+Set Universe Polymorphism.
+Set Printing All.
+Set Implicit Arguments.
+Record prod A B := pair { fst : A ; snd : B }.
+Goal forall x : prod Set Set, let f := @fst _ in f _ x = @fst _ _ x.
+simpl; intros.
+  constr_eq (@fst Set Set x) (fst (A := Set) (B := Set) x).   
+  Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x).
+  reflexivity.
+Qed.
diff --git a/test-suite/bugs/opened/3593.v b/test-suite/bugs/opened/3593.v
deleted file mode 100644
index d83b900607..0000000000
--- a/test-suite/bugs/opened/3593.v
+++ /dev/null
@@ -1,10 +0,0 @@
-Set Universe Polymorphism.
-Set Printing All.
-Set Implicit Arguments.
-Record prod A B := pair { fst : A ; snd : B }.
-Goal forall x : prod Set Set, let f := @fst _ in f _ x = @fst _ _ x.
-simpl; intros.
-  constr_eq (@fst Set Set x) (fst (A := Set) (B := Set) x).   
-  Fail Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x).
-  reflexivity.
-Qed.
-- 
cgit v1.2.3


From 0a2dfa5e5d17ccf58328432888dff345ef0bf5e6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 23 Apr 2015 14:06:19 +0200
Subject: Removing dead code in Pp.

---
 lib/pp.ml  | 21 ---------------------
 lib/pp.mli |  3 ---
 2 files changed, 24 deletions(-)

diff --git a/lib/pp.ml b/lib/pp.ml
index 6e6b32c590..d672f06dbb 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -18,7 +18,6 @@ module Glue : sig
   val empty : 'a t
   val is_empty : 'a t -> bool
   val iter : ('a -> unit) -> 'a t -> unit
-  val map : ('a -> 'b) -> 'a t -> 'b t
 
 end = struct
 
@@ -41,11 +40,6 @@ end = struct
     | GLeaf x -> f x
     | GNode (x,y) -> iter f x; iter f y
 
-  let rec map f = function
-    | GEmpty -> GEmpty
-    | GLeaf x -> GLeaf (f x)
-    | GNode (x,y) -> GNode (map f x, map f y)
-
 end
 
 module Tag :
@@ -156,21 +150,6 @@ let app = Glue.glue
 
 let is_empty g = Glue.is_empty g
 
-let rewrite f p =
-  let strtoken = function
-    | Str_len (s, n) ->
-      let s' = f s in
-      Str_len (s', String.length s')
-    | Str_def s ->
-      Str_def (f s)
-  in
-  let rec ppcmd_token = function
-    | Ppcmd_print x -> Ppcmd_print (strtoken x)
-    | Ppcmd_box (bt, g) -> Ppcmd_box (bt, Glue.map ppcmd_token g)
-    | p -> p
-  in
-  Glue.map ppcmd_token p
-
 (* Compute length of an UTF-8 encoded string
    Rem 1 : utf8_length <= String.length (equal if pure ascii)
    Rem 2 : if used for an iso8859_1 encoded string, the result is
diff --git a/lib/pp.mli b/lib/pp.mli
index 5dd2686d14..e20e5ca82a 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -46,9 +46,6 @@ val eval_ppcmds : std_ppcmds -> std_ppcmds
 val is_empty : std_ppcmds -> bool
 (** Test emptyness. *)
 
-val rewrite : (string -> string) -> std_ppcmds -> std_ppcmds
-(** [rewrite f pps] applies [f] to all strings that appear in [pps]. *)
-
 (** {6 Derived commands} *)
 
 val spc : unit -> std_ppcmds
-- 
cgit v1.2.3


From 915c8f15965fe8e7ee9d02a663fd890ef80539ad Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 23 Apr 2015 14:22:42 +0200
Subject: Using tclZEROMSG instead of tclZERO in several places.

---
 plugins/cc/cctac.ml        |  4 ++--
 plugins/omega/coq_omega.ml |  2 +-
 tactics/auto.ml            |  4 ++--
 tactics/autorewrite.ml     |  4 ++--
 tactics/contradiction.ml   |  4 ++--
 tactics/eauto.ml4          |  2 +-
 tactics/eqdecide.ml        |  4 ++--
 tactics/equality.ml        | 16 ++++++++--------
 tactics/extratactics.ml4   |  4 ++--
 tactics/tacinterp.ml       | 10 ++++------
 tactics/tacticals.ml       |  9 +++------
 tactics/tactics.ml         |  3 +--
 tactics/tauto.ml4          |  4 ++--
 toplevel/auto_ind_decl.ml  | 30 ++++++++++++++----------------
 14 files changed, 46 insertions(+), 54 deletions(-)

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 8884aef1cf..05f4c49030 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -302,9 +302,9 @@ let rec proof_tac p : unit Proofview.tactic =
   	     Tacticals.New.tclFIRST
 	       [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma2 refine)) (proof_tac p2);
 		reflexivity;
-                Proofview.tclZERO (UserError ("Congruence" ,
+                Tacticals.New.tclZEROMSG
 		    (Pp.str
-		       "I don't know how to handle dependent equality")))]]
+		       "I don't know how to handle dependent equality")]]
   | Inject (prf,cstr,nargs,argind) ->
 	 let ti=constr_of_term prf.p_lhs in
 	 let tj=constr_of_term prf.p_rhs in
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 37428c39da..4e2696dfdb 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1462,7 +1462,7 @@ let coq_omega =
       let path = simplify_strong (new_id,new_var_num,display_var) system in
       if !display_action_flag then display_action display_var path;
       Tacticals.New.tclTHEN prelude (replay_history tactic_normalisation path)
-    with NO_CONTRADICTION -> Proofview.tclZERO (UserError ("" , Pp.str"Omega can't solve this system"))
+    with NO_CONTRADICTION -> Tacticals.New.tclZEROMSG (Pp.str"Omega can't solve this system")
   end
   end
 
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 46274f8329..7da8415714 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -131,7 +131,7 @@ let conclPattern concl pat tac =
 	try
 	  Proofview.tclUNIT (Constr_matching.matches env sigma pat concl)
 	with Constr_matching.PatternMatchingFailure ->
-          Proofview.tclZERO (UserError ("conclPattern",str"conclPattern"))
+          Tacticals.New.tclZEROMSG (str "conclPattern")
   in
    Proofview.Goal.enter (fun gl ->
      let env = Proofview.Goal.env gl in
@@ -458,7 +458,7 @@ let search d n mod_delta db_list local_db =
     (* spiwack: the test of [n] to 0 must be done independently in
        each goal. Hence the [tclEXTEND] *)
     Proofview.tclEXTEND [] begin
-      if Int.equal n 0 then Proofview.tclZERO (Errors.UserError ("",str"BOUND 2")) else
+      if Int.equal n 0 then Tacticals.New.tclZEROMSG (str"BOUND 2") else
         Tacticals.New.tclORELSE0 (dbg_assumption d)
 	  (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db)
 	     ( Proofview.Goal.enter begin fun gl ->
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 4eb8a79256..048bd637aa 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -174,7 +174,7 @@ let gen_auto_multi_rewrite conds tac_main lbas cl =
   if cl.concl_occs != AllOccurrences &&
      cl.concl_occs != NoOccurrences
   then
-    Proofview.tclZERO (UserError("" , str"The \"at\" syntax isn't available yet for the autorewrite tactic."))
+    Tacticals.New.tclZEROMSG (str"The \"at\" syntax isn't available yet for the autorewrite tactic.")
   else
     let compose_tac t1 t2 =
       match cl.onhyps with
@@ -204,7 +204,7 @@ let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl =
 	*)
 	gen_auto_multi_rewrite conds tac_main lbas cl
     | _ ->
-        Proofview.tclZERO (UserError ("autorewrite",strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion."))
+        Tacticals.New.tclZEROMSG (strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.")
 
 (* Functions necessary to the library object declaration *)
 let cache_hintrewrite (_,(rbase,lrl)) =
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 9b69481da9..c03710e911 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -55,7 +55,7 @@ let contradiction_context =
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
     let rec seek_neg l = match l with
-      | [] ->  Proofview.tclZERO (UserError ("" , Pp.str"No such contradiction"))
+      | [] ->  Tacticals.New.tclZEROMSG (Pp.str"No such contradiction")
       | (id,_,typ)::rest ->
           let typ = nf_evar sigma typ in
 	  let typ = whd_betadeltaiota env sigma typ in
@@ -107,7 +107,7 @@ let contradiction_term (c,lbind as cl) =
             Proofview.tclZERO Not_found
         end
         begin function (e, info) -> match e with
-          | Not_found -> Proofview.tclZERO (Errors.UserError ("",Pp.str"Not a contradiction."))
+          | Not_found -> Tacticals.New.tclZEROMSG (Pp.str"Not a contradiction.")
           | e -> Proofview.tclZERO ~info e
         end
   end
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 27c3569daf..d738677e50 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -609,7 +609,7 @@ TACTIC EXTEND unify
     match table with
     | None ->
       let msg = str "Hint table " ++ str base ++ str " not found" in
-      Proofview.tclZERO (UserError ("", msg))
+      Tacticals.New.tclZEROMSG msg
     | Some t ->
       let state = Hint_db.transparent_state t in
       unify ~state x y
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index c2cd9e47f1..2ee4bf8e12 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -158,7 +158,7 @@ let solveEqBranch rectype =
       end
     end
     begin function (e, info) -> match e with
-      | PatternMatchingFailure -> Proofview.tclZERO (UserError ("",Pp.str"Unexpected conclusion!"))
+      | PatternMatchingFailure -> Tacticals.New.tclZEROMSG (Pp.str"Unexpected conclusion!")
       | e -> Proofview.tclZERO ~info e
     end
 
@@ -186,7 +186,7 @@ let decideGralEquality =
     end
     begin function (e, info) -> match e with
       | PatternMatchingFailure ->
-          Proofview.tclZERO (UserError ("", Pp.str"The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}."))
+          Tacticals.New.tclZEROMSG (Pp.str"The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}.")
       | e -> Proofview.tclZERO ~info e
     end
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7ab8d0c3ba..816b54f027 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -454,7 +454,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl =
 	(* Otherwise, if we are told to rewrite in all hypothesis via the
            syntax "* |-", we fail iff all the different rewrites fail *)
 	let rec do_hyps_atleastonce = function
-	  | [] -> Proofview.tclZERO (Errors.UserError ("",Pp.str"Nothing to rewrite."))
+	  | [] -> tclZEROMSG (Pp.str"Nothing to rewrite.")
 	  | id :: l ->
 	    tclIFTHENTRYELSEMUST
 	     (general_rewrite_ebindings_in l2r AllOccurrences false true ?tac id c with_evars)
@@ -874,7 +874,7 @@ let gen_absurdity id =
   then
     simplest_elim (mkVar id)
   else
-    Proofview.tclZERO (Errors.UserError ("Equality.gen_absurdity" , str "Not the negation of an equality."))
+    tclZEROMSG (str "Not the negation of an equality.")
   end
 
 (* Precondition: eq is leibniz equality
@@ -936,7 +936,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
     let concl = Proofview.Goal.concl gl in
     match find_positions env sigma t1 t2 with
     | Inr _ ->
-	Proofview.tclZERO (Errors.UserError ("discr" , str"Not a discriminable equality."))
+	tclZEROMSG (str"Not a discriminable equality.")
     | Inl (cpath, (_,dirn), _) ->
 	let sort = pf_apply get_type_of gl concl in
 	discr_positions env sigma u eq_clause cpath dirn sort
@@ -968,7 +968,7 @@ let onNegatedEquality with_evars tac =
           (onLastHypId (fun id ->
             onEquality with_evars tac (mkVar id,NoBindings)))
     | _ ->
-        Proofview.tclZERO (Errors.UserError ("" , str "Not a negated primitive equality."))
+        tclZEROMSG (str "Not a negated primitive equality.")
   end
 
 let discrSimpleClause with_evars = function
@@ -1303,7 +1303,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
   in
   let injectors = List.map_filter filter posns in
   if List.is_empty injectors then
-    Proofview.tclZERO (Errors.UserError ("Equality.inj" , str "Failed to decompose the equality."))
+    tclZEROMSG (str "Failed to decompose the equality.")
   else
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref)
     (Proofview.tclBIND
@@ -1319,12 +1319,12 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
   let env = eq_clause.env in
   match find_positions env sigma t1 t2 with
   | Inl _ ->
-     Proofview.tclZERO (Errors.UserError ("Inj",strbrk"This equality is discriminable. You should use the discriminate tactic to solve the goal."))
+     tclZEROMSG (strbrk"This equality is discriminable. You should use the discriminate tactic to solve the goal.")
   | Inr [] ->
      let suggestion = if !injection_on_proofs then "" else " You can try to use option Set Injection On Proofs." in
-     Proofview.tclZERO (Errors.UserError ("Equality.inj",strbrk("No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop." ^ suggestion)))
+     tclZEROMSG (strbrk("No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop." ^ suggestion))
   | Inr [([],_,_)] when Flags.version_strictly_greater Flags.V8_3 ->
-     Proofview.tclZERO (Errors.UserError ("Equality.inj" , str"Nothing to inject."))
+     tclZEROMSG (str"Nothing to inject.")
   | Inr posns ->
       inject_at_positions env sigma l2r u eq_clause posns
 	(tac (clenv_value eq_clause))
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 7f0a4c6609..f217cda894 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -750,7 +750,7 @@ let rec find_a_destructable_match t =
 
 let destauto t =
   try find_a_destructable_match t;
-    Proofview.tclZERO (UserError ("",  str"No destructable match found"))
+    Tacticals.New.tclZEROMSG (str "No destructable match found")
   with Found tac -> tac
 
 let destauto_in id = 
@@ -966,7 +966,7 @@ let guard tst =
     Proofview.tclUNIT ()
   else
     let msg = Pp.(str"Condition not satisfied:"++ws 1++(pr_itest tst)) in
-    Proofview.tclZERO (Errors.UserError("guard",msg))
+    Tacticals.New.tclZEROMSG msg
 
 
 TACTIC EXTEND guard
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index f29680e185..0a746d283e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1492,11 +1492,11 @@ and tactic_of_value ist vle =
         extra = TacStore.set ist.extra f_trace []; } in
       let tac = name_if_glob appl (eval_tactic ist t) in
       catch_error_tac trace tac
-  | (VFun _|VRec _) -> Proofview.tclZERO (UserError ("" , str "A fully applied tactic is expected."))
+  | (VFun _|VRec _) -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.")
   else if has_type vle (topwit wit_tactic) then
     let tac = out_gen (topwit wit_tactic) vle in
     eval_tactic ist tac
-  else Proofview.tclZERO (UserError ("" , str"Expression does not evaluate to a tactic."))
+  else Tacticals.New.tclZEROMSG (str "Expression does not evaluate to a tactic.")
 
 (* Interprets the clauses of a recursive LetIn *)
 and interp_letrec ist llc u =
@@ -1752,10 +1752,8 @@ and interp_ltac_constr ist e : constr Ftactic.t =
     Ftactic.return cresult
   with CannotCoerceTo _ ->
     let env = Proofview.Goal.env gl in
-    Proofview.tclZERO (UserError ( "",
-      errorlabstrm ""
-      (str "Must evaluate to a closed term" ++ fnl() ++
-      str "offending expression: " ++ fnl() ++ pr_inspect env e result)))
+    Tacticals.New.tclZEROMSG (str "Must evaluate to a closed term" ++ fnl() ++
+      str "offending expression: " ++ fnl() ++ pr_inspect env e result)
   end
 
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 9b16fe3f7b..17ac7a4b66 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -420,7 +420,7 @@ module New = struct
 
   (* Try the first tactic that does not fail in a list of tactics *)
   let rec tclFIRST = function
-    | [] -> tclZERO (Errors.UserError ("Tacticals.New.tclFIRST",str"No applicable tactic."))
+    | [] -> tclZEROMSG (str"No applicable tactic.")
     |  t::rest -> tclORELSE0 t (tclFIRST rest)
 
   let rec tclFIRST_PROGRESS_ON tac = function
@@ -430,10 +430,7 @@ module New = struct
 
   let rec tclDO n t =
     if n < 0 then
-      tclZERO (Errors.UserError (
-        "Refiner.tclDO",
-        str"Wrong argument : Do needs a positive integer.")
-      )
+      tclZEROMSG (str"Wrong argument : Do needs a positive integer.")
     else if n = 0 then tclUNIT ()
     else if n = 1 then t
     else tclTHEN t (tclDO (n-1) t)
@@ -456,7 +453,7 @@ module New = struct
   let tclCOMPLETE t =
     t >>= fun res ->
       (tclINDEPENDENT
-         (tclZERO (Errors.UserError ("",str"Proof is not complete.")))
+         (tclZEROMSG (str"Proof is not complete."))
       ) <*>
         tclUNIT res
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7484139c68..b40c8d0e74 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -751,8 +751,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
 	     (intro_then_gen name_flag move_flag false dep_flag tac))
           begin function (e, info) -> match e with
             | RefinerError IntroNeedsProduct ->
-                Proofview.tclZERO 
-		  (Errors.UserError("Intro",str "No product even after head-reduction."))
+                Tacticals.New.tclZEROMSG (str "No product even after head-reduction.")
             | e -> Proofview.tclZERO ~info e
           end
   end
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 4b03ff249f..b4c7bffa9c 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -316,7 +316,7 @@ let tauto_intuitionistic flags =
     (intuition_gen (default_ist ()) flags <:tactic<fail>>)
     begin function (e, info) -> match e with
       | Refiner.FailError _ | UserError _ ->
-          Proofview.tclZERO (UserError ("tauto" , str "tauto failed."))
+          Tacticals.New.tclZEROMSG (str "tauto failed.")
       | e -> Proofview.tclZERO ~info e
     end
 
@@ -328,7 +328,7 @@ let tauto_classical flags nnpp =
   Proofview.tclORELSE
     (Tacticals.New.tclTHEN (apply nnpp) (tauto_intuitionistic flags))
     begin function (e, info) -> match e with
-      | UserError _ -> Proofview.tclZERO (UserError ("tauto" , str "Classical tauto failed."))
+      | UserError _ -> Tacticals.New.tclZEROMSG (str "Classical tauto failed.")
       | e -> Proofview.tclZERO ~info e
     end
 
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 26b54a73ea..26ff7b92fc 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -369,7 +369,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q =
 	     Printer.pr_constr type_of_pq ++
 	     str " first.")
           in
-          Proofview.tclZERO (Errors.UserError("",err_msg))
+          Tacticals.New.tclZEROMSG err_msg
        in
        lb_type_of_p >>= fun (lb_type_of_p,eff) ->
        let lb_args = Array.append (Array.append
@@ -456,28 +456,28 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
         )
         end
     | ([],[]) -> Proofview.tclUNIT ()
-    | _ -> Proofview.tclZERO (UserError ("" , str"Both side of the equality must have the same arity."))
+    | _ -> Tacticals.New.tclZEROMSG (str "Both side of the equality must have the same arity.")
   in
   begin try Proofview.tclUNIT (destApp lft)
-    with DestKO ->  Proofview.tclZERO (UserError ("" , str"replace failed."))
+    with DestKO -> Tacticals.New.tclZEROMSG (str "replace failed.")
   end >>= fun (ind1,ca1) ->
   begin try Proofview.tclUNIT (destApp rgt)
-    with DestKO -> Proofview.tclZERO (UserError ("" , str"replace failed."))
+    with DestKO -> Tacticals.New.tclZEROMSG (str "replace failed.")
   end >>= fun (ind2,ca2) ->
   begin try Proofview.tclUNIT (out_punivs (destInd ind1))
     with DestKO ->
       begin try Proofview.tclUNIT (fst (fst (destConstruct ind1)))
-        with DestKO -> Proofview.tclZERO (UserError ("" , str"The expected type is an inductive one."))
+        with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.")
       end
   end >>= fun (sp1,i1) ->
   begin try Proofview.tclUNIT (out_punivs (destInd ind2))
     with DestKO ->
       begin try Proofview.tclUNIT (fst (fst (destConstruct ind2)))
-        with DestKO -> Proofview.tclZERO (UserError ("" , str"The expected type is an inductive one."))
+        with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.")
       end
   end >>= fun (sp2,i2) ->
   if not (eq_mind sp1 sp2) || not (Int.equal i1 i2)
-  then Proofview.tclZERO (UserError ("" , str"Eq should be on the same type"))
+  then Tacticals.New.tclZEROMSG (str "Eq should be on the same type")
   else aux (Array.to_list ca1) (Array.to_list ca2)
 
 (*
@@ -610,10 +610,10 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
                                      (ca.(1)))
                                   Auto.default_auto
                               else
-                                Proofview.tclZERO (UserError ("",str"Failure while solving Boolean->Leibniz."))
-                          | _ -> Proofview.tclZERO (UserError ("", str"Failure while solving Boolean->Leibniz."))
+                                Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.")
+                          | _ -> Tacticals.New.tclZEROMSG (str" Failure while solving Boolean->Leibniz.")
                         )
-                        | _ -> Proofview.tclZERO (UserError ("", str"Failure while solving Boolean->Leibniz."))
+                        | _ -> Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.")
                       end
 
                     ]
@@ -733,10 +733,10 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec =
                                 nparrec
                                 ca'.(n-2) ca'.(n-1)
                           | _ ->
-                              Proofview.tclZERO (UserError ("",str"Failure while solving Leibniz->Boolean."))
+                              Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.")
                         )
                         | _ ->
-                            Proofview.tclZERO (UserError ("",str"Failure while solving Leibniz->Boolean."))
+                            Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.")
                       end
                     ]
       end
@@ -856,15 +856,13 @@ let compute_dec_tact ind lnamesparrec nparrec =
           let c, eff = find_scheme bl_scheme_kind ind in
           Proofview.tclUNIT (mkConst c,eff) with
     Not_found ->
-      Proofview.tclZERO (UserError ("",str"Error during the decidability part, boolean to leibniz"++
-        str" equality is required."))
+      Tacticals.New.tclZEROMSG (str "Error during the decidability part, boolean to leibniz equality is required.")
   end >>= fun (blI,eff') ->
   begin try
           let c, eff = find_scheme lb_scheme_kind ind in
           Proofview.tclUNIT (mkConst c,eff) with
     Not_found ->
-      Proofview.tclZERO (UserError ("",str"Error during the decidability part, leibniz to boolean"++
-        str" equality is required."))
+      Tacticals.New.tclZEROMSG (str "Error during the decidability part, leibniz to boolean equality is required.")
   end >>= fun (lbI,eff'') ->
   let eff = (Declareops.union_side_effects eff'' (Declareops.union_side_effects eff' eff)) in
   Tacticals.New.tclTHENLIST [
-- 
cgit v1.2.3


From 16d301bab5b7dec53be4786b3b6815bca54ae539 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 23 Apr 2015 14:55:11 +0200
Subject: Remove almost all the uses of string concatenation when building
 error messages.

Since error messages are ultimately passed to Format, which has its own
buffers for concatenating strings, using concatenation for preparing error
messages just doubles the workload and increases memory pressure.
---
 checker/checker.ml                            | 20 ++++-----
 interp/coqlib.ml                              | 11 ++---
 interp/notation.ml                            | 26 +++++------
 interp/syntax_def.ml                          |  2 +-
 lib/dyn.ml                                    |  9 ++--
 lib/errors.ml                                 |  6 +--
 lib/pp.ml                                     |  2 +-
 lib/system.ml                                 | 11 +++--
 library/declaremods.ml                        |  2 +-
 library/goptions.ml                           | 16 ++++---
 library/impargs.ml                            |  7 ++-
 library/lib.ml                                | 11 +++--
 library/libobject.ml                          |  5 +--
 library/library.ml                            | 29 ++++++------
 parsing/g_xml.ml4                             |  2 +-
 plugins/funind/functional_principles_types.ml | 13 +++---
 plugins/funind/indfun_common.ml               |  4 +-
 plugins/funind/recdef.ml                      |  3 +-
 pretyping/unification.ml                      |  3 +-
 printing/pptactic.ml                          |  9 ++--
 printing/ppvernac.ml                          |  4 +-
 printing/prettyp.ml                           | 16 +++----
 printing/printer.ml                           |  4 +-
 proofs/evar_refiner.ml                        |  5 ++-
 proofs/logic.ml                               | 22 +++++-----
 proofs/redexpr.ml                             | 11 +++--
 proofs/tactic_debug.ml                        | 14 +++---
 tactics/autorewrite.ml                        |  2 +-
 tactics/equality.ml                           |  4 +-
 tactics/hints.ml                              |  2 +-
 tactics/rewrite.ml                            |  2 +-
 tactics/tacenv.ml                             |  8 ++--
 tactics/tacinterp.ml                          |  4 +-
 tactics/tacticals.ml                          |  3 +-
 tactics/tactics.ml                            |  9 ++--
 toplevel/auto_ind_decl.ml                     | 11 +++--
 toplevel/cerrors.ml                           |  8 ++--
 toplevel/command.ml                           | 17 ++++----
 toplevel/coqinit.ml                           |  4 +-
 toplevel/coqloop.ml                           |  2 +-
 toplevel/coqtop.ml                            |  2 +-
 toplevel/himsg.ml                             | 14 +++---
 toplevel/ind_tables.ml                        |  4 +-
 toplevel/locality.ml                          |  5 ++-
 toplevel/metasyntax.ml                        | 25 ++++++-----
 toplevel/mltop.ml                             | 13 +++---
 toplevel/search.ml                            |  8 ++--
 toplevel/vernac.ml                            |  2 +-
 toplevel/vernacentries.ml                     | 63 +++++++++++++--------------
 49 files changed, 258 insertions(+), 221 deletions(-)

diff --git a/checker/checker.ml b/checker/checker.ml
index 9a1007acb3..0f7ed8df51 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -67,13 +67,13 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath =
       Check.add_load_path (dir,coq_dirpath)
     end
   else
-    msg_warning (str ("Cannot open " ^ dir))
+    msg_warning (str "Cannot open " ++ str dir)
 
 let convert_string d =
   try Id.of_string d
   with Errors.UserError _ ->
     if_verbose msg_warning
-      (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)"));
+      (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)");
     raise Exit
 
 let add_rec_path ~unix_path ~coq_root =
@@ -90,7 +90,7 @@ let add_rec_path ~unix_path ~coq_root =
     List.iter Check.add_load_path dirs;
     Check.add_load_path (unix_path, coq_root)
   else
-    msg_warning (str ("Cannot open " ^ unix_path))
+    msg_warning (str "Cannot open " ++ str unix_path)
 
 (* By the option -include -I or -R of the command line *)
 let includes = ref []
@@ -221,7 +221,7 @@ let print_loc loc =
   else
     let loc = Loc.unloc loc in
     (int (fst loc) ++ str"-" ++ int (snd loc))
-let guill s = "\""^s^"\""
+let guill s = str "\"" ++ str s ++ str "\""
 
 let where s =
   if !Flags.debug then  (str"in " ++ str s ++ str":" ++ spc ()) else (mt ())
@@ -232,7 +232,7 @@ let rec explain_exn = function
   | Stream.Error txt ->
       hov 0 (str "Syntax error: " ++ str txt)
   | Sys_error msg ->
-      hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report() )
+      hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ guill msg ++ report() )
   | UserError(s,pps) ->
       hov 1 (str "User error: " ++ where s ++ pps)
   | Out_of_memory ->
@@ -241,14 +241,14 @@ let rec explain_exn = function
       hov 0 (str "Stack overflow")
   | Match_failure(filename,pos1,pos2) ->
       hov 1 (anomaly_string () ++ str "Match failure in file " ++
-	     str (guill filename) ++ str " at line " ++ int pos1 ++
+	     guill filename ++ str " at line " ++ int pos1 ++
 	     str " character " ++ int pos2 ++ report ())
   | Not_found ->
       hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report ())
   | Failure s ->
       hov 0 (str "Failure: " ++ str s ++ report ())
   | Invalid_argument s ->
-      hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report ())
+      hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ guill s ++ report ())
   | Sys.Break ->
       hov 0 (fnl () ++ str "User interrupt.")
   | Univ.UniverseInconsistency (o,u,v) ->
@@ -294,7 +294,7 @@ let rec explain_exn = function
           Format.printf "@\n====== universes ====@\n";
           Pp.pp (Univ.pr_universes
             (ctx.Environ.env_stratification.Environ.env_universes));
-          str("\nCantApplyBadType at argument " ^ string_of_int n)
+          str "\nCantApplyBadType at argument " ++ int n
       | CantApplyNonFunctional _ -> str"CantApplyNonFunctional"
       | IllFormedRecBody _ -> str"IllFormedRecBody"
       | IllTypedRecBody _ -> str"IllTypedRecBody"
@@ -309,7 +309,7 @@ let rec explain_exn = function
       hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++
 	       (if s = "" then mt ()
 		else
-		  (str ("(file \"" ^ s ^ "\", line ") ++ int b ++
+		  (str "(file \"" ++ str s ++ str "\", line " ++ int b ++
 		   str ", characters " ++ int e ++ str "-" ++
 		   int (e+6) ++ str ")")) ++
 	       report ())
@@ -323,7 +323,7 @@ let parse_args argv =
 
     | "-coqlib" :: s :: rem ->
       if not (exists_dir s) then 
-	fatal_error (str ("Directory '"^s^"' does not exist")) false;
+	fatal_error (str "Directory '" ++ str s ++ str "' does not exist") false;
       Flags.coqlib := s;
       Flags.coqlib_spec := true;
       parse rem
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 02504c9202..5ac718e3b0 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -54,15 +54,15 @@ let gen_reference_in_modules locstr dirs s =
   match these with
     | [x] -> x
     | [] ->
-	anomaly ~label:locstr (str ("cannot find "^s^
-	" in module"^(if List.length dirs > 1 then "s " else " ")) ++
+	anomaly ~label:locstr (str "cannot find " ++ str s ++
+	str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++
 	prlist_with_sep pr_comma pr_dirpath dirs)
     | l ->
       anomaly ~label:locstr
-	(str ("ambiguous name "^s^" can represent ") ++
+	(str "ambiguous name " ++ str s ++ str " can represent " ++
 	   prlist_with_sep pr_comma
 	   (fun x -> Libnames.pr_path (Nametab.path_of_global x)) l ++
-	   str (" in module"^(if List.length dirs > 1 then "s " else " ")) ++
+	   str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++
 	   prlist_with_sep pr_comma pr_dirpath dirs)
 
 let gen_constant_in_modules locstr dirs s =
@@ -86,7 +86,8 @@ let check_required_library d =
      (Loc.ghost,make_qualid (DirPath.make (List.rev prefix)) m)
 *)
 (* or failing ...*)
-      error ("Library "^(DirPath.to_string dir)^" has to be required first.")
+      errorlabstrm "Coqlib.check_required_library"
+        (str "Library " ++ str (DirPath.to_string dir) ++ str " has to be required first.")
 
 (************************************************************************)
 (* Specific Coq objects *)
diff --git a/interp/notation.ml b/interp/notation.ml
index 80db2cb396..555dfa804b 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -91,7 +91,9 @@ let declare_scope scope =
 (*    Flags.if_warn message ("Creating scope "^scope);*)
     scope_map := String.Map.add scope empty_scope !scope_map
 
-let error_unknown_scope sc = error ("Scope "^sc^" is not declared.")
+let error_unknown_scope sc =
+  errorlabstrm "Notation"
+    (str "Scope " ++ str sc ++ str " is not declared.")
 
 let find_scope scope =
   try String.Map.find scope !scope_map
@@ -186,14 +188,14 @@ let declare_delimiters scope key =
     | Some oldkey when String.equal oldkey key -> ()
     | Some oldkey ->
 	msg_warning
-	  (strbrk ("Overwriting previous delimiting key "^oldkey^" in scope "^scope));
+	  (str "Overwriting previous delimiting key " ++ str oldkey ++ str " in scope " ++ str scope);
 	scope_map := String.Map.add scope newsc !scope_map
   end;
   try
     let oldscope = String.Map.find key !delimiters_map in
     if String.equal oldscope scope then ()
     else begin
-      msg_warning (strbrk ("Hiding binding of key "^key^" to "^oldscope));
+      msg_warning (str "Hiding binding of key " ++ str key ++ str " to " ++ str oldscope);
       delimiters_map := String.Map.add key scope !delimiters_map
     end
   with Not_found -> delimiters_map := String.Map.add key scope !delimiters_map
@@ -202,7 +204,7 @@ let find_delimiters_scope loc key =
   try String.Map.find key !delimiters_map
   with Not_found ->
     user_err_loc
-    (loc, "find_delimiters", str ("Unknown scope delimiting key "^key^"."))
+    (loc, "find_delimiters", str "Unknown scope delimiting key " ++ str key ++ str ".")
 
 (* Uninterpretation tables *)
 
@@ -317,8 +319,7 @@ let check_required_module loc sc (sp,d) =
   try let _ = Nametab.global_of_path sp in ()
   with Not_found ->
     user_err_loc (loc,"prim_token_interpreter",
-    str ("Cannot interpret in "^sc^" without requiring first module "
-    ^(List.last d)^"."))
+    str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".")
 
 (* Look if some notation or numeral printer in [scope] can be used in
    the scope stack [scopes], and if yes, using delimiters or not *)
@@ -373,10 +374,9 @@ let declare_notation_interpretation ntn scopt pat df =
   let () =
     if String.Map.mem ntn sc.notations then
     let which_scope = match scopt with
-    | None -> ""
-    | Some _ -> " in scope " ^ scope in
-    let message = "Notation " ^ ntn ^ " was already used" ^ which_scope in
-    msg_warning (strbrk message)
+    | None -> mt ()
+    | Some _ -> str " in scope " ++ str scope in
+    msg_warning (str "Notation " ++ str ntn ++ str " was already used" ++ which_scope)
   in
   let sc = { sc with notations = String.Map.add ntn (pat,df) sc.notations } in
   let () = scope_map := String.Map.add scope sc !scope_map in
@@ -452,7 +452,7 @@ let interp_notation loc ntn local_scopes =
   try find_interpretation ntn (find_notation ntn) scopes
   with Not_found ->
     user_err_loc
-    (loc,"",str ("Unknown interpretation for notation \""^ntn^"\"."))
+    (loc,"",str "Unknown interpretation for notation \"" ++ str ntn ++ str "\".")
 
 let uninterp_notations c =
   List.map_append (fun key -> keymap_find key !notations_key_table)
@@ -784,8 +784,8 @@ let pr_scope_classes sc =
   match l with
   | [] -> mt ()
   | _ :: l ->
-    let opt_s = match l with [] -> "" | _ -> "es" in
-    hov 0 (str ("Bound to class" ^ opt_s) ++
+    let opt_s = match l with [] -> mt () | _ -> str "es" in
+    hov 0 (str "Bound to class" ++ opt_s ++
       spc() ++ prlist_with_sep spc pr_scope_class l) ++ fnl()
 
 let pr_notation_info prglob ntn c =
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 9be7abcfe0..d2709d5e3c 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -99,7 +99,7 @@ let verbose_compat kn def = function
       | [], NRef r -> str " is " ++ pr_global_env Id.Set.empty r
       | _ -> str " is a compatibility notation"
     in
-    let since = str (" since Coq > " ^ Flags.pr_version v ^ ".") in
+    let since = str " since Coq > " ++ str (Flags.pr_version v) ++ str "." in
     act (pr_syndef kn ++ pp_def ++ since)
   | _ -> ()
 
diff --git a/lib/dyn.ml b/lib/dyn.ml
index a5e8fb9c2b..056b687313 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Errors
+open Pp
 
 (* Dynamics, programmed with DANGER !!! *)
 
@@ -23,7 +24,7 @@ let create (s : string) =
   let () =
     if Int.Map.mem hash !dyntab then
       let old = Int.Map.find hash !dyntab in
-      let msg = Pp.str ("Dynamic tag collision: " ^ s ^ " vs. " ^ old) in
+      let msg = str "Dynamic tag collision: " ++ str s ++ str " vs. " ++ str old in
       anomaly ~label:"Dyn.create" msg
   in
   let () = dyntab := Int.Map.add hash s !dyntab in
@@ -31,8 +32,7 @@ let create (s : string) =
   let outfun (nh, rv) =
     if Int.equal hash nh then Obj.magic rv
     else
-      let msg = (Pp.str ("dyn_out: expected " ^ s)) in
-      anomaly msg
+      anomaly (str "dyn_out: expected " ++ str s)
   in
   (infun, outfun)
 
@@ -43,8 +43,7 @@ let has_tag (s, _) tag =
 let tag (s,_) =
   try Int.Map.find s !dyntab
   with Not_found ->
-    let msg = Pp.str ("Unknown dynamic tag " ^ (string_of_int s)) in
-    anomaly msg
+    anomaly (str "Unknown dynamic tag " ++ int s)
 
 let pointer_equal (t1,o1) (t2,o2) = t1 = t2 && o1 == o2
 
diff --git a/lib/errors.ml b/lib/errors.ml
index 13f3916477..999d99ee08 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -69,12 +69,12 @@ let rec print_gen bottom stk e =
 let where = function
 | None -> mt ()
 | Some s ->
-  if !Flags.debug then str ("in "^s^":") ++ spc () else mt ()
+  if !Flags.debug then str "in " ++ str s ++ str ":" ++ spc () else mt ()
 
 let raw_anomaly e = match e with
   | Anomaly (s, pps) -> where s ++ pps ++ str "."
-  | Assert_failure _ | Match_failure _ -> str (Printexc.to_string e ^ ".")
-  | _ -> str ("Uncaught exception " ^ Printexc.to_string e ^ ".")
+  | Assert_failure _ | Match_failure _ -> str (Printexc.to_string e) ++ str "."
+  | _ -> str "Uncaught exception " ++ str (Printexc.to_string e) ++ str "."
 
 let print_backtrace e = match Backtrace.get_backtrace e with
 | None -> mt ()
diff --git a/lib/pp.ml b/lib/pp.ml
index d672f06dbb..9667f7270e 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -249,7 +249,7 @@ let escape_string s =
     else escape_at s (i-1) in
   escape_at s (String.length s - 1)
 
-let qstring s = str ("\""^escape_string s^"\"")
+let qstring s = str "\"" ++ str (escape_string s) ++ str "\""
 let qs = qstring
 let quote s = h 0 (str "\"" ++ s ++ str "\"")
 
diff --git a/lib/system.ml b/lib/system.ml
index 73095f9cd6..d1cdd8efc9 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -118,7 +118,8 @@ let is_in_system_path filename =
 
 let open_trapping_failure name =
   try open_out_bin name
-  with e when Errors.noncritical e -> error ("Can't open " ^ name)
+  with e when Errors.noncritical e ->
+    errorlabstrm "System.open" (str "Can't open " ++ str name)
 
 let try_remove filename =
   try Sys.remove filename
@@ -126,7 +127,8 @@ let try_remove filename =
     msg_warning
       (str"Could not remove file " ++ str filename ++ str" which is corrupted!")
 
-let error_corrupted file s = error (file ^": " ^ s ^ ". Try to rebuild it.")
+let error_corrupted file s =
+  errorlabstrm "System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.")
 
 let input_binary_int f ch =
   try input_binary_int ch
@@ -201,7 +203,8 @@ let extern_intern ?(warn=true) magic =
 	let reraise = Errors.push reraise in
         let () = try_remove filename in
         iraise reraise
-    with Sys_error s -> error ("System error: " ^ s)
+    with Sys_error s ->
+      errorlabstrm "System.extern_state" (str "System error: " ++ str s)
   and intern_state paths name =
     try
       let _,filename = find_file_in_path ~warn paths name in
@@ -210,7 +213,7 @@ let extern_intern ?(warn=true) magic =
       close_in channel;
       v
     with Sys_error s ->
-      error("System error: " ^ s)
+      errorlabstrm "System.intern_state" (str "System error: " ++ str s)
   in
   (extern_state,intern_state)
 
diff --git a/library/declaremods.ml b/library/declaremods.ml
index cc7c4d7f11..a82f5260ba 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -950,7 +950,7 @@ type 'modast module_params =
 let debug_print_modtab _ =
   let pr_seg = function
     | [] -> str "[]"
-    | l -> str ("[." ^ string_of_int (List.length l) ^ ".]")
+    | l -> str "[." ++ int (List.length l) ++ str ".]"
   in
   let pr_modinfo mp (prefix,substobjs,keepobjs) s =
     s ++ str (string_of_mp mp) ++ (spc ())
diff --git a/library/goptions.ml b/library/goptions.ml
index ef25fa5902..4f50fbfbdd 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -35,7 +35,7 @@ type option_state = {
 let nickname table = String.concat " " table
 
 let error_undeclared_key key =
-  error ((nickname key)^": no table or option of this type")
+  errorlabstrm "Goptions" (str (nickname key) ++ str ": no table or option of this type")
 
 (****************************************************************************)
 (* 1- Tables                                                                *)
@@ -301,7 +301,9 @@ let declare_string_option =
 let set_option_value locality check_and_cast key v =
   let (name, depr, (_,read,write,lwrite,gwrite)) =
     try get_option key
-    with Not_found -> error ("There is no option "^(nickname key)^".")
+    with Not_found ->
+      errorlabstrm "Goptions.set_option_value"
+        (str "There is no option " ++ str (nickname key) ++ str ".")
   in
   let write = match locality with
     | None -> write
@@ -364,9 +366,9 @@ let print_option_value key =
   let s = read () in
   match s with
     | BoolValue b ->
-	msg_info (str ("The "^name^" mode is "^(if b then "on" else "off")))
+	msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off"))
     | _ ->
-	msg_info (str ("Current value of "^name^" is ") ++ msg_option_value (name, s))
+	msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s))
 
 let get_tables () =
   let tables = !value_tab in
@@ -383,7 +385,7 @@ let get_tables () =
 
 let print_tables () =
   let print_option key name value depr =
-    let msg = str ("  "^(nickname key)^": ") ++ msg_option_value (name, value) in
+    let msg = str "  " ++ str (nickname key) ++ str ": " ++ msg_option_value (name, value) in
     if depr then msg ++ str " [DEPRECATED]" ++ fnl ()
     else msg ++ fnl ()
   in
@@ -401,10 +403,10 @@ let print_tables () =
       !value_tab (mt ()) ++
   str "Tables:" ++ fnl () ++
     List.fold_right
-      (fun (nickkey,_) p -> p ++ str ("  "^nickkey) ++ fnl ())
+      (fun (nickkey,_) p -> p ++ str "  " ++ str nickkey ++ fnl ())
       !string_table (mt ()) ++
     List.fold_right
-      (fun (nickkey,_) p -> p ++ str ("  "^nickkey) ++ fnl ())
+      (fun (nickkey,_) p -> p ++ str "  " ++ str nickkey ++ fnl ())
       !ref_table (mt ()) ++
     fnl ()
 
diff --git a/library/impargs.ml b/library/impargs.ml
index 4b0e2e3d1a..94f53219e7 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -10,6 +10,7 @@ open Errors
 open Util
 open Names
 open Globnames
+open Nameops
 open Term
 open Reduction
 open Declarations
@@ -337,10 +338,12 @@ let check_correct_manual_implicits autoimps l =
   List.iter (function
     | ExplByName id,(b,fi,forced) ->
 	if not forced then
-	  error ("Wrong or non-dependent implicit argument name: "^(Id.to_string id)^".")
+	  errorlabstrm ""
+            (str "Wrong or non-dependent implicit argument name: " ++ pr_id id ++ str ".")
     | ExplByPos (i,_id),_t ->
 	if i<1 || i>List.length autoimps then
-	  error ("Bad implicit argument number: "^(string_of_int i)^".")
+	  errorlabstrm ""
+            (str "Bad implicit argument number: " ++ int i ++ str ".")
 	else
 	  errorlabstrm ""
 	    (str "Cannot set implicit argument number " ++ int i ++
diff --git a/library/lib.ml b/library/lib.ml
index 9977b66654..81db547efd 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -75,7 +75,8 @@ let classify_segment seg =
     | (_,ClosedModule _) :: stk -> clean acc stk
     | (_,OpenedSection _) :: _ -> error "there are still opened sections"
     | (_,OpenedModule (ty,_,_,_)) :: _ ->
-      error ("there are still opened " ^ module_kind ty ^"s")
+      errorlabstrm "Lib.classify_segment"
+        (str "there are still opened " ++ str (module_kind ty) ++ str "s")
     | (_,FrozenState _) :: stk -> clean acc stk
   in
     clean ([],[],[]) (List.rev seg)
@@ -274,7 +275,7 @@ let start_modtype = start_mod true None
 let error_still_opened string oname =
   let id = basename (fst oname) in
   errorlabstrm ""
-    (str ("The "^string^" ") ++ pr_id id ++ str " is still opened.")
+    (str "The " ++ str string ++ str " " ++ pr_id id ++ str " is still opened.")
 
 let end_mod is_type =
   let oname,fs =
@@ -318,7 +319,8 @@ let end_compilation_checks dir =
     try match snd (find_entry_p is_opening_node) with
       | OpenedSection _ -> error "There are some open sections."
       | OpenedModule (ty,_,_,_) ->
-	error ("There are some open "^module_kind ty^"s.")
+	errorlabstrm "Lib.end_compilation_checks"
+          (str "There are some open " ++ str (module_kind ty) ++ str "s.")
       | _ -> assert false
     with Not_found -> ()
   in
@@ -369,7 +371,8 @@ let find_opening_node id =
     let oname,entry = find_entry_p is_opening_node in
     let id' = basename (fst oname) in
     if not (Names.Id.equal id id') then
-      error ("Last block to end has name "^(Names.Id.to_string id')^".");
+      errorlabstrm "Lib.find_opening_node"
+        (str "Last block to end has name " ++ pr_id id' ++ str ".");
     entry
   with Not_found -> error "There is nothing to end."
 
diff --git a/library/libobject.ml b/library/libobject.ml
index 5f2a2127d9..74930d76ec 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Libnames
+open Pp
 
 (* The relax flag is used to make it possible to load files while ignoring
    failures to incorporate some objects.  This can be useful when one
@@ -33,15 +34,13 @@ type 'a object_declaration = {
   discharge_function : object_name * 'a -> 'a option;
   rebuild_function : 'a -> 'a }
 
-let yell s = Errors.anomaly (Pp.str s)
-
 let default_object s = {
   object_name = s;
   cache_function = (fun _ -> ());
   load_function = (fun _ _ -> ());
   open_function = (fun _ _ -> ());
   subst_function = (fun _ ->
-    yell ("The object "^s^" does not know how to substitute!"));
+    Errors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!"));
   classify_function = (fun obj -> Keep obj);
   discharge_function = (fun _ -> None);
   rebuild_function = (fun x -> x)}
diff --git a/library/library.ml b/library/library.ml
index b4261309fd..1ffa1a305c 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -126,7 +126,8 @@ let find_library dir =
 let try_find_library dir =
   try find_library dir
   with Not_found ->
-    error ("Unknown library " ^ (DirPath.to_string dir))
+    errorlabstrm "Library.find_library"
+      (str "Unknown library " ++ str (DirPath.to_string dir))
 
 let register_library_filename dir f =
   (* Not synchronized: overwrite the previous binding if one existed *)
@@ -378,10 +379,10 @@ let access_table what tables dp i =
       let t =
         try fetch_delayed f
         with Faulty f ->
-          error
-            ("The file "^f^" (bound to " ^ dir_path ^
-            ") is inaccessible or corrupted,\n" ^
-            "cannot load some "^what^" in it.\n")
+          errorlabstrm "Library.access_table"
+            (str "The file " ++ str f ++ str " (bound to " ++ str dir_path ++
+             str ") is inaccessible or corrupted,\ncannot load some " ++
+             str what ++ str " in it.\n")
       in
       tables := LibraryMap.add dp (Fetched t) !tables;
       t
@@ -462,7 +463,7 @@ let rec intern_library (needed, contents) (dir, f) from =
   let m = intern_from_file f in
   if not (DirPath.equal dir m.library_name) then
     errorlabstrm "load_physical_library"
-      (str ("The file " ^ f ^ " contains library") ++ spc () ++
+      (str "The file " ++ str f ++ str " contains library" ++ spc () ++
        pr_dirpath m.library_name ++ spc () ++ str "and not library" ++
        spc() ++ pr_dirpath dir);
   Pp.feedback(Feedback.FileLoaded(DirPath.to_string dir, f));
@@ -475,9 +476,7 @@ and intern_library_deps libs dir m from =
 and intern_mandatory_library caller from libs (dir,d) =
   let digest, libs = intern_library libs (try_locate_absolute_library dir) from in
   if not (Safe_typing.digest_match ~actual:digest ~required:d) then
-    errorlabstrm "" (strbrk ("Compiled library "^ DirPath.to_string caller ^
-      ".vo makes inconsistent assumptions over library " ^
-      DirPath.to_string dir));
+    errorlabstrm "" (str "Compiled library " ++ str (DirPath.to_string caller) ++ str ".vo makes inconsistent assumptions over library " ++ str (DirPath.to_string dir));
   libs
 
 let rec_intern_library libs mref =
@@ -487,7 +486,7 @@ let rec_intern_library libs mref =
 let check_library_short_name f dir = function
   | Some id when not (Id.equal id (snd (split_dirpath dir))) ->
       errorlabstrm "check_library_short_name"
-      (str ("The file " ^ f ^ " contains library") ++ spc () ++
+      (str "The file " ++ str f ++ str " contains library" ++ spc () ++
       pr_dirpath dir ++ spc () ++ str "and not library" ++ spc () ++
       pr_id id)
   | _ -> ()
@@ -613,7 +612,7 @@ let safe_locate_module (loc,qid) =
   try Nametab.locate_module qid
   with Not_found ->
     user_err_loc
-      (loc,"import_library", str (string_of_qualid qid ^ " is not a module"))
+      (loc,"import_library", str (string_of_qualid qid) ++ str " is not a module")
 
 let import_module export modl =
   (* Optimization: libraries in a raw in the list are imported
@@ -638,7 +637,7 @@ let import_module export modl =
             try Declaremods.import_module export mp; aux [] l
             with Not_found ->
               user_err_loc (loc,"import_library",
-                str ((string_of_qualid dir)^" is not a module")))
+                str (string_of_qualid dir) ++ str " is not a module"))
     | [] -> flush acc
   in aux [] modl
 
@@ -650,8 +649,8 @@ let check_coq_overwriting p id =
   let is_empty = match l with [] -> true | _ -> false in
   if not !Flags.boot && not is_empty && String.equal (Id.to_string (List.last l)) "Coq" then
     errorlabstrm ""
-      (strbrk ("Cannot build module "^DirPath.to_string p^"."^Id.to_string id^
-      ": it starts with prefix \"Coq\" which is reserved for the Coq library."))
+      (str "Cannot build module " ++ str (DirPath.to_string p) ++ str "." ++ pr_id id ++ str "." ++ spc () ++
+      str "it starts with prefix \"Coq\" which is reserved for the Coq library.")
 
 (* Verifies that a string starts by a letter and do not contain
    others caracters than letters, digits, or `_` *)
@@ -795,7 +794,7 @@ let save_library_to ?todo dir f otab =
         msg_error (str"Could not compile the library to native code. Skipping.")
    with reraise ->
     let reraise = Errors.push reraise in
-    let () = msg_warning (str ("Removed file "^f')) in
+    let () = msg_warning (str "Removed file " ++ str f') in
     let () = close_out ch in
     let () = Sys.remove f' in
     iraise reraise
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 84e4a5732e..992f9c59af 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -58,7 +58,7 @@ END
 
 let error_bad_arity loc n =
   let s = match n with 0 -> "none" | 1 -> "one" | 2 -> "two" | _ -> "many" in
-  user_err_loc (loc,"",str ("wrong number of arguments (expect "^s^")."))
+  user_err_loc (loc,"",str "wrong number of arguments (expect " ++ str s ++ str ").")
 
 (* Interpreting attributes *)
 
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 45e5aaf545..a2bbf97ae3 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -604,7 +604,8 @@ let build_scheme fas =
 	      try
 		Smartlocate.global_with_alias f
 	      with Not_found ->
-	      	Errors.error ("Cannot find "^ Libnames.string_of_reference f)
+                errorlabstrm "FunInd.build_scheme"
+                  (str "Cannot find " ++ Libnames.pr_reference f)
 	    in
 	    let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in
 	    let evd',_ = Typing.e_type_of ~refresh:true (Global.env ()) evd' f in 
@@ -636,10 +637,12 @@ let build_case_scheme fa =
 (*   let id_to_constr id =  *)
 (*     Constrintern.global_reference  id *)
 (*   in  *)
-  let funs =  (fun (_,f,_) ->
-		 try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f))
-		 with Not_found ->
-		   Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in
+  let funs =
+    let (_,f,_) = fa in
+    try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f))
+    with Not_found ->
+      errorlabstrm "FunInd.build_case_scheme"
+        (str "Cannot find " ++ Libnames.pr_reference f) in
   let first_fun,u = destConst  funs in
   let funs_mp,funs_dp,_ = Names.repr_con first_fun in
   let first_fun_kn = try fst (find_Function_infos  first_fun).graph_ind with Not_found -> raise No_graph_found in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 738ade8ca3..1c409500ef 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -109,7 +109,9 @@ let const_of_id id =
     qualid_of_reference (Libnames.Ident (Loc.ghost,id))
   in
   try Constrintern.locate_reference princ_ref
-  with Not_found -> Errors.error ("cannot find "^ Id.to_string id)
+  with Not_found ->
+    Errors.errorlabstrm "IndFun.const_of_id"
+      (str "cannot find " ++ Nameops.pr_id id)
 
 let def_of_const t =
    match (Term.kind_of_term t) with
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 0999b95d71..b9902a9fc7 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -305,7 +305,8 @@ let check_not_nested forbidden e =
       | Rel _ -> ()
       | Var x ->
         if Id.List.mem x forbidden
-        then error ("check_not_nested : failure "^Id.to_string x)
+        then errorlabstrm "Recdef.check_not_nested"
+               (str "check_not_nested: failure " ++ pr_id x)
       | Meta _ | Evar _ | Sort _ -> ()
       | Cast(e,_,t) -> check_not_nested e;check_not_nested t
       | Prod(_,t,b) -> check_not_nested t;check_not_nested b
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 01e1154e58..c2281e13a5 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1528,7 +1528,8 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
     let ids = ids_of_named_context (named_context env) in
     if name == Anonymous then next_ident_away_in_goal x ids else
     if mem_named_context x (named_context env) then
-      error ("The variable "^(Id.to_string x)^" is already declared.")
+      errorlabstrm "Unification.make_abstraction_core"
+        (str "The variable " ++ Nameops.pr_id x ++ str " is already declared.")
     else
       x
   in
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index f8264e5af6..a669aef9a8 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1260,13 +1260,12 @@ module Make
 
         and pr_tacarg = function
           | TacDynamic (loc,t) ->
-            pr_with_comments loc (
-              str "<" ++ keyword "dynamic" ++ str (" [" ^ (Dyn.tag t)^"]>")
-            )
+            pr_with_comments loc
+              (str "<" ++ keyword "dynamic" ++ str " [" ++ str (Dyn.tag t) ++ str "]>")
           | MetaIdArg (loc,true,s) ->
-            pr_with_comments loc (str ("$" ^ s))
+            pr_with_comments loc (str "$" ++ str s)
           | MetaIdArg (loc,false,s) ->
-            pr_with_comments loc (keyword "constr:" ++ str(" $" ^ s))
+            pr_with_comments loc (keyword "constr:" ++ str " $" ++ str s)
           | Reference r ->
             pr.pr_reference r
           | ConstrMayEval c ->
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 89ffae4b3e..c6b1b672f8 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1253,7 +1253,7 @@ module Make
     and pr_extend s cl =
       let pr_arg a =
         try pr_gen a
-        with Failure _ -> str ("<error in "^fst s^">") in
+        with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in
       try
         let rl = Egramml.get_extend_vernac_rule s in
         let start,rl,cl =
@@ -1271,7 +1271,7 @@ module Make
             (start,cl) rl in
         hov 1 pp
       with Not_found ->
-        hov 1 (str ("TODO("^fst s) ++ prlist_with_sep sep pr_arg cl ++ str ")")
+        hov 1 (str "TODO(" ++ str (fst s) ++ prlist_with_sep sep pr_arg cl ++ str ")")
 
     in pr_vernac
 
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 4a66c33df8..e50435cda2 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -180,16 +180,16 @@ let print_opacity ref =
     | None -> []
     | Some s ->
        [pr_global ref ++ str " is " ++
-        str (match s with
-          | FullyOpaque -> "opaque"
+        match s with
+          | FullyOpaque -> str "opaque"
           | TransparentMaybeOpacified Conv_oracle.Opaque ->
-              "basically transparent but considered opaque for reduction"
+              str "basically transparent but considered opaque for reduction"
           | TransparentMaybeOpacified lev when Conv_oracle.is_transparent lev ->
-              "transparent"
+              str "transparent"
           | TransparentMaybeOpacified (Conv_oracle.Level n) ->
-              "transparent (with expansion weight "^string_of_int n^")"
+              str "transparent (with expansion weight " ++ int n ++ str ")"
           | TransparentMaybeOpacified Conv_oracle.Expand ->
-              "transparent (with minimal expansion weight)")]
+              str "transparent (with minimal expansion weight)"]
 
 (*******************)
 (* *)
@@ -386,9 +386,9 @@ let print_located_qualid name flags ref =
     | [] ->
 	let (dir,id) = repr_qualid qid in
 	if DirPath.is_empty dir then
-	  str ("No " ^ name ^ " of basename") ++ spc () ++ pr_id id
+	  str "No " ++ str name ++ str " of basename" ++ spc () ++ pr_id id
 	else
-	  str ("No " ^ name ^ " of suffix") ++ spc () ++ pr_qualid qid
+	  str "No " ++ str name ++ str " of suffix" ++ spc () ++ pr_qualid qid
     | l ->
 	prlist_with_sep fnl
 	(fun (o,oqid) ->
diff --git a/printing/printer.ml b/printing/printer.ml
index 0d3a1c17e4..141ae145dd 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -654,7 +654,7 @@ let pr_goal_by_id id =
   let p = Proof_global.give_me_the_proof () in
   let g = Goal.get_by_uid id in
   let pr gs =
-    v 0 (str ("goal / evar " ^ id ^ " is:") ++ cut ()
+    v 0 (str "goal / evar " ++ str id ++ str " is:" ++ cut ()
 	 ++ pr_goal gs)
   in
   try
@@ -723,7 +723,7 @@ let pr_assumptionset env s =
       try pr_constant env kn
       with Not_found ->
 	let mp,_,lab = repr_con kn in
-	str (string_of_mp mp ^ "." ^ Label.to_string lab)
+        str (string_of_mp mp) ++ str "." ++ pr_label lab
     in
     let safe_pr_ltype typ =
       try str " : " ++ pr_ltype typ
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index c8cb1d1cc2..9b358210a0 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -12,6 +12,7 @@ open Names
 open Evd
 open Evarutil
 open Evarsolve
+open Pp
 
 (******************************************)
 (* Instantiation of existential variables *)
@@ -54,8 +55,8 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
     with e when Errors.noncritical e ->
       let loc = Glob_ops.loc_of_glob_constr rawc in
       user_err_loc
-        (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^
-			string_of_existential evk))
+        (loc,"", str "Instance is not well-typed in the environment of " ++
+                 str (string_of_existential evk))
   in
   define_and_solve_constraints evk typed_c env (evars_reset_evd sigma' sigma)
 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index b8206ca1b5..898588d9e4 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -179,7 +179,8 @@ let check_decl_position env sign (x,_,_ as d) =
   let needed = global_vars_set_of_decl env d in
   let deps = dependency_closure env (named_context_of_val sign) needed in
   if Id.List.mem x deps then
-    error ("Cannot create self-referring hypothesis "^Id.to_string x);
+    errorlabstrm "Logic.check_decl_position"
+      (str "Cannot create self-referring hypothesis " ++ pr_id x);
   x::deps
 
 (* Auxiliary functions for primitive MOVE tactic
@@ -488,9 +489,11 @@ let convert_hyp check sign sigma (id,b,bt as d) =
       (fun _ (_,c,ct) _ ->
         let env = Global.env_of_context sign in
         if check && not (is_conv env sigma bt ct) then
-	  error ("Incorrect change of the type of "^(Id.to_string id)^".");
+	  errorlabstrm "Logic.convert_hyp"
+            (str "Incorrect change of the type of " ++ pr_id id ++ str ".");
         if check && not (Option.equal (is_conv env sigma) b c) then
-	  error ("Incorrect change of the body of "^(Id.to_string id)^".");
+	  errorlabstrm "Logic.convert_hyp"
+            (str "Incorrect change of the body of "++ pr_id id ++ str ".");
        if check then reorder := check_decl_position env sign d;
        d) in
   reorder_val_context env sign' !reorder
@@ -522,7 +525,8 @@ let prim_refiner r sigma goal =
 	      t,cl,sigma
 	  else
             (if !check && mem_named_context id (named_context_of_val sign) then
-	      error ("Variable " ^ Id.to_string id ^ " is already declared.");
+	      errorlabstrm "Logic.prim_refiner"
+                (str "Variable " ++ pr_id id ++ str " is already declared.");
 	     push_named_context_val (id,None,t) sign,t,cl,sigma) in
         let (sg2,ev2,sigma) = 
 	  Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in
@@ -550,11 +554,10 @@ let prim_refiner r sigma goal =
 	  | (f,n,ar)::oth ->
 	      let ((sp',_),u')  = check_ind env n ar in
 	      if not (eq_mind sp sp') then
-		error ("Fixpoints should be on the same " ^
-		       "mutual inductive declaration.");
+		error "Fixpoints should be on the same mutual inductive declaration.";
 	      if !check && mem_named_context f (named_context_of_val sign) then
-		error
-		  ("Name "^Id.to_string f^" already used in the environment");
+		errorlabstrm "Logic.prim_refiner"
+		  (str "Name " ++ pr_id f ++ str " already used in the environment");
 	      mk_sign (push_named_context_val (f,None,ar) sign) oth
 	  | [] ->
 	      Evd.Monad.List.map (fun (_,_,c) sigma ->
@@ -584,8 +587,7 @@ let prim_refiner r sigma goal =
 		try
 		  let _ = find_coinductive env sigma b in ()
                 with Not_found ->
-		  error ("All methods must construct elements " ^
-			  "in coinductive types.")
+		  error "All methods must construct elements in coinductive types."
 	in
 	let firsts,lasts = List.chop j others in
 	let all = firsts@(f,cl)::lasts in
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 1383d75567..d25f7e9150 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -167,18 +167,20 @@ let red_expr_tab = Summary.ref String.Map.empty ~name:"Declare Reduction"
 
 let declare_reduction s f =
   if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab
-  then error ("There is already a reduction expression of name "^s)
+  then errorlabstrm "Redexpr.declare_reduction"
+    (str "There is already a reduction expression of name " ++ str s)
   else reduction_tab := String.Map.add s f !reduction_tab
 
 let check_custom = function
   | ExtraRedExpr s ->
       if not (String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab)
-      then error ("Reference to undefined reduction expression "^s)
+      then errorlabstrm "Redexpr.check_custom" (str "Reference to undefined reduction expression " ++ str s)
   |_ -> ()
 
 let decl_red_expr s e =
   if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab
-  then error ("There is already a reduction expression of name "^s)
+  then errorlabstrm "Redexpr.decl_red_expr"
+    (str "There is already a reduction expression of name " ++ str s)
   else begin
     check_custom e;
     red_expr_tab := String.Map.add s e !red_expr_tab
@@ -232,7 +234,8 @@ let reduction_of_red_expr env =
       with Not_found ->
 	(try reduction_of_red_expr (String.Map.find s !red_expr_tab)
 	 with Not_found ->
-	   error("unknown user-defined reduction \""^s^"\"")))
+	   errorlabstrm "Redexpr.reduction_of_red_expr"
+             (str "unknown user-defined reduction \"" ++ str s ++ str "\"")))
   | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast)
   | CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast)
   in
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 3cc81daf58..d7f4b5ead5 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -11,6 +11,7 @@ open Names
 open Pp
 open Tacexpr
 open Termops
+open Nameops
 
 let (prtac, tactic_printer) = Hook.make ()
 let (prmatchpatt, match_pattern_printer) = Hook.make ()
@@ -231,17 +232,16 @@ let db_pattern_rule debug num r =
 
 (* Prints the hypothesis pattern identifier if it exists *)
 let hyp_bound = function
-  | Anonymous -> " (unbound)"
-  | Name id -> " (bound to "^(Names.Id.to_string id)^")"
+  | Anonymous -> str " (unbound)"
+  | Name id -> str " (bound to " ++ pr_id id ++ str ")"
 
 (* Prints a matched hypothesis *)
 let db_matched_hyp debug env (id,_,c) ido =
   let open Proofview.NonLogical in
   is_debug debug >>= fun db ->
   if db then
-    msg_tac_debug (str "Hypothesis " ++
-           str ((Names.Id.to_string id)^(hyp_bound ido)^
-                " has been matched: ") ++ print_constr_env env c)
+    msg_tac_debug (str "Hypothesis " ++ pr_id id ++ hyp_bound ido ++
+                str " has been matched: " ++ print_constr_env env c)
   else return ()
 
 (* Prints the matched conclusion *)
@@ -266,8 +266,8 @@ let db_hyp_pattern_failure debug env sigma (na,hyp) =
   let open Proofview.NonLogical in
   is_debug debug >>= fun db ->
   if db then
-    msg_tac_debug (str ("The pattern hypothesis"^(hyp_bound na)^
-                " cannot match: ") ++
+    msg_tac_debug (str "The pattern hypothesis" ++ hyp_bound na ++
+                str " cannot match: " ++
            Hook.get prmatchpatt env sigma hyp)
   else return ()
 
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 048bd637aa..ad8164fa64 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -66,7 +66,7 @@ let find_base bas =
   try raw_find_base bas
   with Not_found ->
     errorlabstrm "AutoRewrite"
-      (str ("Rewriting base "^(bas)^" does not exist."))
+      (str "Rewriting base " ++ str bas ++ str " does not exist.")
 
 let find_rewrites bas =
   List.rev_map snd (HintDN.find_all (find_base bas))
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 816b54f027..5d6fcc5b10 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -306,8 +306,8 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
 	      let _ = Global.lookup_constant c1' in
 		c1'
 	    with Not_found -> 
-	      let rwr_thm = Label.to_string l' in 
-	      error ("Cannot find rewrite principle "^rwr_thm^".")
+	      errorlabstrm "Equality.find_elim"
+                (str "Cannot find rewrite principle " ++ pr_label l' ++ str ".")
 	  end
 	| _ -> destConstRef pr1
         end
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 55d62e1514..f83aa56017 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -598,7 +598,7 @@ let current_pure_db () =
   List.map snd (Hintdbmap.bindings (Hintdbmap.remove "v62" !searchtable))
 
 let error_no_such_hint_database x =
-  error ("No such Hint database: "^x^".")
+  errorlabstrm "Hints" (str "No such Hint database: " ++ str x ++ str ".")
 
 (**************************************************************************)
 (*                       Definition of the summary                        *)
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index ac8b4923e5..60ce0e0dc3 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -52,7 +52,7 @@ let try_find_global_reference dir s =
   let sp = Libnames.make_path (make_dir ("Coq"::dir)) (Id.of_string s) in
     try Nametab.global_of_path sp
     with Not_found -> 
-      anomaly (str ("Global reference " ^ s ^ " not found in generalized rewriting"))
+      anomaly (str "Global reference " ++ str s ++ str " not found in generalized rewriting")
 
 let find_reference dir s =
   let gr = lazy (try_find_global_reference dir s) in
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index 84c0a99b18..ffff44d5bc 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -43,7 +43,7 @@ end
 module MLTacMap = Map.Make(MLName)
 
 let pr_tacname t =
-  t.mltac_plugin ^ "::" ^ t.mltac_tactic
+  str t.mltac_plugin ++ str "::" ++ str t.mltac_tactic
 
 let tac_tab = ref MLTacMap.empty
 
@@ -52,9 +52,9 @@ let register_ml_tactic ?(overwrite = false) s (t : ml_tactic) =
     if MLTacMap.mem s !tac_tab then
       if overwrite then
         let () = tac_tab := MLTacMap.remove s !tac_tab in
-        msg_warning (str ("Overwriting definition of tactic " ^ pr_tacname s))
+        msg_warning (str "Overwriting definition of tactic " ++ pr_tacname s)
       else
-        Errors.anomaly (str ("Cannot redeclare tactic " ^ pr_tacname s ^ "."))
+        Errors.anomaly (str "Cannot redeclare tactic " ++ pr_tacname s ++ str ".")
   in
   tac_tab := MLTacMap.add s t !tac_tab
 
@@ -63,7 +63,7 @@ let interp_ml_tactic s =
     MLTacMap.find s !tac_tab
   with Not_found ->
     Errors.errorlabstrm ""
-      (str "The tactic " ++ str (pr_tacname s) ++ str " is not installed.")
+      (str "The tactic " ++ pr_tacname s ++ str " is not installed.")
 
 (***************************************************************************)
 (* Tactic registration *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 0a746d283e..7ce158fd1a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1040,8 +1040,8 @@ let read_pattern lfun ist env sigma = function
 let cons_and_check_name id l =
   if Id.List.mem id l then
     user_err_loc (dloc,"read_match_goal_hyps",
-      strbrk ("Hypothesis pattern-matching variable "^(Id.to_string id)^
-      " used twice in the same pattern."))
+      str "Hypothesis pattern-matching variable " ++ pr_id id ++
+      str " used twice in the same pattern.")
   else id::l
 
 let rec read_match_goal_hyps lfun ist env sigma lidh = function
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 17ac7a4b66..5ba53a7641 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -615,7 +615,8 @@ module New = struct
 	    | Var id -> string_of_id id
 	    | _ -> "\b"
 	  in
-	  error ("The elimination combinator " ^ name_elim ^ " is unknown.")
+	  errorlabstrm "Tacticals.general_elim_then_using"
+            (str "The elimination combinator " ++ str name_elim ++ str " is unknown.")
     in
     let elimclause' = clenv_fchain indmv elimclause indclause in
     let branchsigns = compute_construtor_signatures isrec ind in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b40c8d0e74..8117e4131b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -139,7 +139,8 @@ let introduction ?(check=true) id =
     let store = Proofview.Goal.extra gl in
     let env = Proofview.Goal.env gl in
     let () = if check && mem_named_context id hyps then
-      error ("Variable " ^ Id.to_string id ^ " is already declared.")
+      errorlabstrm "Tactics.introduction"
+        (str "Variable " ++ pr_id id ++ str " is already declared.")
     in
     match kind_of_term (whd_evar sigma concl) with
     | Prod (_, t, b) -> unsafe_intro env store (id, None, t) b
@@ -1870,8 +1871,8 @@ let check_number_of_constructors expctdnumopt i nconstr =
   if Int.equal i 0 then error "The constructors are numbered starting from 1.";
   begin match expctdnumopt with
     | Some n when not (Int.equal n nconstr) ->
-	error ("Not an inductive goal with "^
-	       string_of_int n ^ String.plural n " constructor"^".")
+	errorlabstrm "Tactics.check_number_of_constructors"
+          (str "Not an inductive goal with " ++ int n ++ str (String.plural n " constructor") ++ str ".")
     | _ -> ()
   end;
   if i > nconstr then error "Not enough constructors."
@@ -3042,7 +3043,7 @@ let make_up_names n ind_opt cname =
 
 let error_ind_scheme s =
   let s = if not (String.is_empty s) then s^" " else s in
-  error ("Cannot recognize "^s^"an induction scheme.")
+  errorlabstrm "Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.")
 
 let glob = Universes.constr_of_global
 
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 26ff7b92fc..96bb89e2a4 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -19,6 +19,7 @@ open Termops
 open Declarations
 open Names
 open Globnames
+open Nameops
 open Inductiveops
 open Tactics
 open Ind_tables
@@ -338,7 +339,8 @@ let do_replace_lb lb_scheme_key aavoid narg p q =
     let rec find i =
       if Id.equal avoid.(n-i) s then avoid.(n-i-x)
       else (if i<n then find (i+1)
-            else error ("Var "^(Id.to_string s)^" seems unknown.")
+            else errorlabstrm "AutoIndDecl.do_replace_lb"
+                   (str "Var " ++ pr_id s ++ str " seems unknown.")
       )
     in mkVar (find 1)
   with e when Errors.noncritical e ->
@@ -395,7 +397,8 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
     let rec find i =
       if Id.equal avoid.(n-i) s then avoid.(n-i-x)
       else (if i<n then find (i+1)
-            else error ("Var "^(Id.to_string s)^" seems unknown.")
+            else errorlabstrm "AutoIndDecl.do_replace_bl"
+                   (str "Var " ++ pr_id s ++ str " seems unknown.")
       )
     in mkVar (find 1)
   with e when Errors.noncritical e ->
@@ -502,8 +505,8 @@ let eqI ind l =
                            (List.map (fun (_,seq,_,_)-> mkVar seq) list_id ))
   and e, eff = 
     try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff 
-    with Not_found -> error
-        ("The boolean equality on "^(string_of_mind (fst ind))^" is needed.");
+    with Not_found -> errorlabstrm "AutoIndDecl.eqI"
+      (str "The boolean equality on " ++ pr_mind (fst ind) ++ str " is needed.");
   in (if Array.equal eq_constr eA [||] then e else mkApp(e,eA)), eff
 
 (**********************************************************************)
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index b29ba1efc5..a0892bed9a 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -20,7 +20,7 @@ let print_loc loc =
     let loc = Loc.unloc loc in
     (int (fst loc) ++ str"-" ++ int (snd loc))
 
-let guill s = "\""^s^"\""
+let guill s = str "\"" ++ str s ++ str "\""
 
 (** Invariant : exceptions embedded in EvaluatedError satisfy
     Errors.noncritical *)
@@ -33,10 +33,10 @@ exception EvaluatedError of std_ppcmds * exn option
 
 let explain_exn_default = function
   (* Basic interaction exceptions *)
-  | Stream.Error txt -> hov 0 (str ("Syntax error: " ^ txt ^ "."))
-  | Compat.Token.Error txt ->  hov 0 (str ("Syntax error: " ^ txt ^ "."))
+  | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".")
+  | Compat.Token.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".")
   | Lexer.Error.E err -> hov 0 (str (Lexer.Error.to_string err))
-  | Sys_error msg -> hov 0 (str ("System error: " ^ guill msg))
+  | Sys_error msg -> hov 0 (str "System error: " ++ guill msg)
   | Out_of_memory -> hov 0 (str "Out of memory.")
   | Stack_overflow -> hov 0 (str "Stack overflow.")
   | Timeout -> hov 0 (str "Timeout!")
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 754ad85261..cdeecf1bb7 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -609,8 +609,7 @@ let declare_mutual_inductive_with_eliminations mie impls =
   begin match mie.mind_entry_finite with
   | BiFinite when is_recursive mie ->
       if Option.has_some mie.mind_entry_record then
-        error ("Records declared with the keywords Record or Structure cannot be recursive." ^
-                  "You can, however, define recursive records using the Inductive or CoInductive command.")
+        error "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command."
       else
         error ("Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command.")
   | _ -> ()
@@ -697,19 +696,19 @@ let rec partial_order cmp = function
 let non_full_mutual_message x xge y yge isfix rest =
   let reason =
     if Id.List.mem x yge then
-      Id.to_string y^" depends on "^Id.to_string x^" but not conversely"
+      pr_id y ++ str " depends on " ++ pr_id x ++ str " but not conversely"
     else if Id.List.mem y xge then
-      Id.to_string x^" depends on "^Id.to_string y^" but not conversely"
+      pr_id x ++ str " depends on " ++ pr_id y ++ str " but not conversely"
     else
-      Id.to_string y^" and "^Id.to_string x^" are not mutually dependent" in
-  let e = if List.is_empty rest then reason else "e.g.: "^reason in
+      pr_id y ++ str " and " ++ pr_id x ++ str " are not mutually dependent" in
+  let e = if List.is_empty rest then reason else str "e.g., " ++ reason in
   let k = if isfix then "fixpoint" else "cofixpoint" in
   let w =
     if isfix
-    then strbrk "Well-foundedness check may fail unexpectedly." ++ fnl()
+    then str "Well-foundedness check may fail unexpectedly." ++ fnl()
     else mt () in
-  strbrk ("Not a fully mutually defined "^k) ++ fnl () ++
-  strbrk ("("^e^").") ++ fnl () ++ w
+  str "Not a fully mutually defined " ++ str k ++ fnl () ++
+  str "(" ++ e ++ str ")." ++ fnl () ++ w
 
 let check_mutuality env isfix fixl =
   let names = List.map fst fixl in
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index f1d8a4923c..19d4363ab8 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -134,6 +134,6 @@ let get_compat_version = function
   | "8.3" -> Flags.V8_3
   | "8.2" -> Flags.V8_2
   | ("8.1" | "8.0") as s ->
-    msg_warning (strbrk ("Compatibility with version "^s^" not supported."));
+    msg_warning (str "Compatibility with version " ++ str s ++ str " not supported.");
     Flags.V8_2
-  | s -> Errors.error ("Unknown compatibility version \""^s^"\".")
+  | s -> Errors.errorlabstrm "get_compat_version" (str "Unknown compatibility version \"" ++ str s ++ str "\".")
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 52fa9e01e0..caaf8054b8 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -176,7 +176,7 @@ let print_location_in_file {outer=s;inner=fname} loc =
     try
       let (line, bol) = line_of_pos 1 0 0 in
       hov 0 (* No line break so as to follow emacs error message format *)
-        (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++
+        (errstrm ++ str"File " ++ str "\"" ++ str fname ++ str "\"" ++
            str", line " ++ int line ++ str", characters " ++
            Cerrors.print_loc (Loc.make_loc (bp-bol,ep-bol))) ++ str":" ++
         fnl ()
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index e9e86953b3..2df7c69c86 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -38,7 +38,7 @@ let get_version_date () =
 
 let print_header () =
   let (ver,rev) = get_version_date () in
-  ppnl (str ("Welcome to Coq "^ver^" ("^rev^")"));
+  ppnl (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")");
   pp_flush ()
 
 let warning s = msg_warning (strbrk s)
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 5429e6608d..ac8ca3a11d 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -872,11 +872,11 @@ let explain_not_match_error = function
       quote (Univ.pr_constraints (Evd.pr_evd_level Evd.empty) cst)
 
 let explain_signature_mismatch l spec why =
-  str "Signature components for label " ++ str (Label.to_string l) ++
+  str "Signature components for label " ++ pr_label l ++
   str " do not match:" ++ spc () ++ explain_not_match_error why ++ str "."
 
 let explain_label_already_declared l =
-  str ("The label "^Label.to_string l^" is already declared.")
+  str "The label " ++ pr_label l ++ str " is already declared."
 
 let explain_application_to_not_path _ =
   strbrk "A module cannot be applied to another module application or " ++
@@ -1170,18 +1170,18 @@ let explain_bad_constructor env cstr ind =
   str "is expected."
 
 let decline_string n s =
-  if Int.equal n 0 then "no "^s^"s"
-  else if Int.equal n 1 then "1 "^s
-  else (string_of_int n^" "^s^"s")
+  if Int.equal n 0 then str "no " ++ str s ++ str "s"
+  else if Int.equal n 1 then str "1 " ++ str s
+  else (int n ++ str " " ++ str s ++ str "s")
 
 let explain_wrong_numarg_constructor env cstr n =
   str "The constructor " ++ pr_constructor env cstr ++
   str " (in type " ++ pr_inductive env (inductive_of_constructor cstr) ++
-  str ") expects " ++ str (decline_string n "argument") ++ str "."
+  str ") expects " ++ decline_string n "argument" ++ str "."
 
 let explain_wrong_numarg_inductive env ind n =
   str "The inductive type " ++ pr_inductive env ind ++
-  str " expects " ++ str (decline_string n "argument") ++ str "."
+  str " expects " ++ decline_string n "argument" ++ str "."
 
 let explain_unused_clause env pats =
 (* Without localisation
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 138e5189a9..0d39466ede 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -23,6 +23,7 @@ open Util
 open Declare
 open Entries
 open Decl_kinds
+open Pp
 
 (**********************************************************************)
 (* Registering schemes in the environment *)
@@ -87,7 +88,8 @@ let declare_scheme_object s aux f =
   try
     let _ = Hashtbl.find scheme_object_table key in
 (*    let aux_msg = if aux="" then "" else " (with key "^aux^")" in*)
-    error ("Scheme object "^key^" already declared.")
+    errorlabstrm "IndTables.declare_scheme_object"
+      (str "Scheme object " ++ str key ++ str " already declared.")
   with Not_found ->
     Hashtbl.add scheme_object_table key (s,f);
     key
diff --git a/toplevel/locality.ml b/toplevel/locality.ml
index f711dad94a..1145a20bbc 100644
--- a/toplevel/locality.ml
+++ b/toplevel/locality.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Pp
+
 (** * Managing locality *)
 
 let local_of_bool = function
@@ -16,7 +18,8 @@ let check_locality locality_flag =
   match locality_flag with
   | Some b ->
     let s = if b then "Local" else "Global" in
-    Errors.error ("This command does not support the \""^s^"\" prefix.")
+    Errors.errorlabstrm "Locality.check_locality"
+      (str "This command does not support the \"" ++ str s ++ str "\" prefix.")
   | None -> ()
 
 (** Extracting the locality flag *)
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 639ec1e6e3..f4fabc4d3a 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -387,7 +387,8 @@ let rec find_pattern nt xl = function
   | _, Break s :: _ | Break s :: _, _ ->
       error ("A break occurs on one side of \"..\" but not on the other side.")
   | _, Terminal s :: _ | Terminal s :: _, _ ->
-      error ("The token \""^s^"\" occurs on one side of \"..\" but not on the other side.")
+      errorlabstrm "Metasyntax.find_pattern"
+        (str "The token \"" ++ str s ++ str "\" occurs on one side of \"..\" but not on the other side.")
   | _, [] ->
       error msg_expected_form_of_recursive_notation
   | ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) ->
@@ -448,7 +449,8 @@ let rec get_notation_vars = function
       let vars = get_notation_vars sl in
       if Id.equal id ldots_var then vars else
 	if Id.List.mem id vars then
-	  error ("Variable "^Id.to_string id^" occurs more than once.")
+	  errorlabstrm "Metasyntax.get_notation_vars"
+            (str "Variable " ++ pr_id id ++ str " occurs more than once.")
 	else
           id::vars
   | (Terminal _ | Break _) :: sl -> get_notation_vars sl
@@ -461,8 +463,8 @@ let analyze_notation_tokens l =
   recvars, List.subtract Id.equal vars (List.map snd recvars), l
 
 let error_not_same_scope x y =
-  error ("Variables "^Id.to_string x^" and "^Id.to_string y^
-    " must be in the same scope.")
+  errorlabstrm "Metasyntax.error_not_name_scope"
+    (str "Variables " ++ pr_id x ++ str " and " ++ pr_id y ++ str " must be in the same scope.")
 
 (**********************************************************************)
 (* Build pretty-printing rules                                        *)
@@ -710,7 +712,7 @@ let is_not_small_constr = function
 let rec define_keywords_aux = function
   | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(IDENT k) :: l
       when is_not_small_constr e ->
-      Flags.if_verbose msg_info (strbrk ("Identifier '"^k^"' now a keyword"));
+      Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
       Lexer.add_keyword k;
       n1 :: GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
   | n :: l -> n :: define_keywords_aux l
@@ -719,7 +721,7 @@ let rec define_keywords_aux = function
   (* Ensure that IDENT articulation terminal symbols are keywords *)
 let define_keywords = function
   | GramConstrTerminal(IDENT k)::l ->
-      Flags.if_verbose msg_info (strbrk ("Identifier '"^k^"' now a keyword"));
+      Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
       Lexer.add_keyword k;
       GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
   | l -> define_keywords_aux l
@@ -804,7 +806,7 @@ let pr_level ntn (from,args) =
 
 let error_incompatible_level ntn oldprec prec =
   errorlabstrm ""
-    (str ("Notation "^ntn^" is already defined") ++ spc() ++
+    (str "Notation " ++ str ntn ++ str " is already defined" ++ spc() ++
     pr_level ntn oldprec ++
     spc() ++ str "while it is now required to be" ++ spc() ++
     pr_level ntn prec ++ str ".")
@@ -871,14 +873,16 @@ let interp_modifiers modl =
     | SetEntryType (s,typ) :: l ->
 	let id = Id.of_string s in
 	if Id.List.mem_assoc id etyps then
-	  error (s^" is already assigned to an entry or constr level.");
+	  errorlabstrm "Metasyntax.interp_modifiers"
+            (str s ++ str " is already assigned to an entry or constr level.");
 	interp assoc level ((id,typ)::etyps) format extra l
     | SetItemLevel ([],n) :: l ->
 	interp assoc level etyps format extra l
     | SetItemLevel (s::idl,n) :: l ->
 	let id = Id.of_string s in
 	if Id.List.mem_assoc id etyps then
-	  error (s^" is already assigned to an entry or constr level.");
+	  errorlabstrm "Metasyntax.interp_modifiers"
+            (str s ++ str " is already assigned to an entry or constr level.");
 	let typ = ETConstr (n,()) in
 	interp assoc level ((id,typ)::etyps) format extra (SetItemLevel (idl,n)::l)
     | SetLevel n :: l ->
@@ -905,7 +909,8 @@ let check_infix_modifiers modifiers =
 let check_useless_entry_types recvars mainvars etyps =
   let vars = let (l1,l2) = List.split recvars in l1@l2@mainvars in
   match List.filter (fun (x,etyp) -> not (List.mem x vars)) etyps with
-  | (x,_)::_ -> error (Id.to_string x ^ " is unbound in the notation.")
+  | (x,_)::_ -> errorlabstrm "Metasyntax.check_useless_entry_types"
+                  (pr_id x ++ str " is unbound in the notation.")
   | _ -> ()
 
 let no_syntax_modifiers = function
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index 0b6fc48c47..a7fb7a58f2 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -164,7 +164,7 @@ let add_rec_ml_dir unix_path =
 let convert_string d =
   try Names.Id.of_string d
   with UserError _ ->
-    msg_warning (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)"));
+    msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)");
     raise Exit
 
 let add_rec_path ~unix_path ~coq_root ~implicit =
@@ -184,7 +184,7 @@ let add_rec_path ~unix_path ~coq_root ~implicit =
     let () = List.iter add dirs in
     Loadpath.add_load_path unix_path ~implicit coq_root
   else
-    msg_warning (str ("Cannot open " ^ unix_path))
+    msg_warning (str "Cannot open " ++ str unix_path)
 
 (* convertit un nom quelconque en nom de fichier ou de module *)
 let mod_of_name name =
@@ -321,13 +321,13 @@ let reset_loaded_modules () = loaded_modules := []
 let if_verbose_load verb f name ?path fname =
   if not verb then f name ?path fname
   else
-    let info = "[Loading ML file "^fname^" ..." in
+    let info = str "[Loading ML file " ++ str fname ++ str " ..." in
     try
       let path = f name ?path fname in
-      msg_info (str (info^" done]"));
+      msg_info (info ++ str " done]");
       path
     with reraise ->
-      msg_info (str (info^" failed]"));
+      msg_info (info ++ str " failed]");
       raise reraise
 
 (** Load a module for the first time (i.e. dynlink it)
@@ -340,7 +340,8 @@ let trigger_ml_object verb cache reinit ?path name =
     add_loaded_module name (known_module_path name);
     if cache then perform_cache_obj name
   end else if not has_dynlink then
-    error ("Dynamic link not supported (module "^name^")")
+    errorlabstrm "Mltop.trigger_ml_object"
+      (str "Dynamic link not supported (module " ++ str name ++ str ")")
   else begin
     let file = file_of_name (Option.default name path) in
     let path =
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 59283edf9f..9e67eef008 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -32,7 +32,7 @@ module SearchBlacklist =
       let key = ["Search";"Blacklist"]
       let title = "Current search blacklist : "
       let member_message s b =
-	str ("Search blacklist does "^(if b then "" else "not ")^"include "^s)
+	str "Search blacklist does " ++ (if b then mt () else str "not ") ++ str "include " ++ str s
       let synchronous = true
      end)
 
@@ -253,7 +253,8 @@ let interface_search flags =
     let regexp =
       try Str.regexp s
       with e when Errors.noncritical e ->
-        Errors.error ("Invalid regexp: " ^ s)
+        Errors.errorlabstrm "Search.interface_search"
+          (str "Invalid regexp: " ++ str s)
     in
     extract_flags ((regexp, b) :: name) tpe subtpe mods blacklist l
   | (Type_Pattern s, b) :: l ->
@@ -271,7 +272,8 @@ let interface_search flags =
     let id =
       try Nametab.full_name_module qid
       with Not_found ->
-        Errors.error ("Module " ^ path ^ " not found.")
+        Errors.errorlabstrm "Search.interface_search"
+          (str "Module " ++ str path ++ str " not found.")
     in
     extract_flags name tpe subtpe ((id, b) :: mods) blacklist l
   | (Include_Blacklist, b) :: l ->
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 176a6c3330..b3694d0e98 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -208,7 +208,7 @@ let display_cmd_header loc com =
   let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com)))
   in
   Pp.pp (str "Chars " ++ int start ++ str " - " ++ int stop ++
-	 str (" ["^cmd^"] "));
+	 str " [" ++ str cmd ++ str "] ");
   Pp.flush_all ()
 
 let rec vernac_com verbosely checknav (loc,com) =
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index cfa9bddc6e..f33c71d8a6 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -351,7 +351,7 @@ let dump_universes_gen g s =
   try
     Univ.dump_universes output_constraint g;
     close ();
-    msg_info (str ("Universes written to file \""^s^"\"."))
+    msg_info (str "Universes written to file \"" ++ str s ++ str "\".")
   with reraise ->
     let reraise = Errors.push reraise in
     close ();
@@ -610,16 +610,14 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast =
   let binders_ast = List.map
    (fun (export,idl,ty) ->
      if not (Option.is_empty export) then
-      error ("Arguments of a functor declaration cannot be exported. " ^
-       "Remove the \"Export\" and \"Import\" keywords from every functor " ^
-       "argument.")
+      error "Arguments of a functor declaration cannot be exported. Remove the \"Export\" and \"Import\" keywords from every functor argument."
      else (idl,ty)) binders_ast in
   let mp =
     Declaremods.declare_module Modintern.interp_module_ast
       id binders_ast (Enforce mty_ast) []
   in
   Dumpglob.dump_moddef loc mp "mod";
-  if_verbose msg_info (str ("Module "^ Id.to_string id ^" is declared"));
+  if_verbose msg_info (str "Module " ++ pr_id id ++ str " is declared");
   Option.iter (fun export -> vernac_import export [Ident (Loc.ghost,id)]) export
 
 let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
@@ -641,7 +639,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
        in
        Dumpglob.dump_moddef loc mp "mod";
        if_verbose msg_info
-         (str ("Interactive Module "^ Id.to_string id ^" started"));
+         (str "Interactive Module " ++ pr_id id ++ str " started");
        List.iter
          (fun (export,id) ->
            Option.iter
@@ -651,9 +649,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
        let binders_ast = List.map
         (fun (export,idl,ty) ->
           if not (Option.is_empty export) then
-           error ("Arguments of a functor definition can be imported only if" ^
-                  " the definition is interactive. Remove the \"Export\" and " ^
-                  "\"Import\" keywords from every functor argument.")
+           error "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument."
           else (idl,ty)) binders_ast in
        let mp =
          Declaremods.declare_module Modintern.interp_module_ast
@@ -661,14 +657,14 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
        in
        Dumpglob.dump_moddef loc mp "mod";
        if_verbose msg_info
-	 (str ("Module "^ Id.to_string id ^" is defined"));
+	 (str "Module " ++ pr_id id ++ str " is defined");
        Option.iter (fun export -> vernac_import export [Ident (Loc.ghost,id)])
          export
 
 let vernac_end_module export (loc,id as lid) =
   let mp = Declaremods.end_module () in
   Dumpglob.dump_modref loc mp "mod";
-  if_verbose msg_info (str ("Module "^ Id.to_string id ^" is defined"));
+  if_verbose msg_info (str "Module " ++ pr_id id ++ str " is defined");
   Option.iter (fun export -> vernac_import export [Ident lid]) export
 
 let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
@@ -690,7 +686,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
        in
        Dumpglob.dump_moddef loc mp "modtype";
        if_verbose msg_info
-	 (str ("Interactive Module Type "^ Id.to_string id ^" started"));
+	 (str "Interactive Module Type " ++ pr_id id ++ str " started");
        List.iter
          (fun (export,id) ->
            Option.iter
@@ -701,9 +697,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
 	let binders_ast = List.map
           (fun (export,idl,ty) ->
             if not (Option.is_empty export) then
-              error ("Arguments of a functor definition can be imported only if" ^
-			" the definition is interactive. Remove the \"Export\" " ^
-			"and \"Import\" keywords from every functor argument.")
+              error "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument."
             else (idl,ty)) binders_ast in
 	let mp =
           Declaremods.declare_modtype Modintern.interp_module_ast
@@ -711,12 +705,12 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
         in
         Dumpglob.dump_moddef loc mp "modtype";
 	if_verbose msg_info
-	  (str ("Module Type "^ Id.to_string id ^" is defined"))
+	  (str "Module Type " ++ pr_id id ++ str " is defined")
 
 let vernac_end_modtype (loc,id) =
   let mp = Declaremods.end_modtype () in
   Dumpglob.dump_modref loc mp "modtype";
-  if_verbose msg_info (str ("Module Type "^ Id.to_string id ^" is defined"))
+  if_verbose msg_info (str "Module Type " ++ pr_id id ++ str " is defined")
 
 let vernac_include l =
   Declaremods.declare_include Modintern.interp_module_ast l
@@ -868,7 +862,8 @@ let vernac_set_used_variables e =
   let vars = Environ.named_context env in
   List.iter (fun id -> 
     if not (List.exists (fun (id',_,_) -> Id.equal id id') vars) then
-      error ("Unknown variable: " ^ Id.to_string id))
+      errorlabstrm "vernac_set_used_variables"
+        (str "Unknown variable: " ++ pr_id id))
     l;
   let closure_l = List.map pi1 (set_used_variables l) in
   let closure_l = List.fold_right Id.Set.add closure_l Id.Set.empty in
@@ -914,7 +909,7 @@ let vernac_chdir = function
   | Some path ->
       begin
 	try Sys.chdir (expand path)
-	with Sys_error err -> msg_warning (str ("Cd failed: " ^ err))
+	with Sys_error err -> msg_warning (str "Cd failed: " ++ str err)
       end;
       if_verbose msg_info (str (Sys.getcwd()))
 
@@ -1051,15 +1046,16 @@ let vernac_declare_arguments locality r l nargs flags =
   let inf_names =
     let ty = Global.type_of_global_unsafe sr in
       Impargs.compute_implicits_names (Global.env ()) ty in
-  let string_of_name = function Anonymous -> "_" | Name id -> Id.to_string id in
   let rec check li ld ls = match li, ld, ls with
     | [], [], [] -> ()
     | [], Anonymous::ld, (Some _)::ls when extra_scope_flag -> check li ld ls
     | [], _::_, (Some _)::ls when extra_scope_flag ->
        error "Extra notation scopes can be set on anonymous arguments only"
-    | [], x::_, _ -> error ("Extra argument " ^ string_of_name x ^ ".")
-    | l, [], _ -> error ("The following arguments are not declared: " ^
-       (String.concat ", " (List.map string_of_name l)) ^ ".")
+    | [], x::_, _ -> errorlabstrm "vernac_declare_arguments"
+                       (str "Extra argument " ++ pr_name x ++ str ".")
+    | l, [], _ -> errorlabstrm "vernac_declare_arguments"
+                    (str "The following arguments are not declared: " ++
+                       prlist_with_sep pr_comma pr_name l ++ str ".")
     | _::li, _::ld, _::ls -> check li ld ls 
     | _ -> assert false in
   let () = match l with
@@ -1087,9 +1083,6 @@ let vernac_declare_arguments locality r l nargs flags =
   let renamed_arg = ref None in
   let set_renamed a b =
     if Option.is_empty !renamed_arg && not (Id.equal a b) then renamed_arg := Some(b,a) in
-  let pr_renamed_arg () = match !renamed_arg with None -> ""
-    | Some (o,n) ->
-       "\nArgument "^string_of_id o ^" renamed to "^string_of_id n^"." in
   let some_renaming_specified =
     try
       let names = Arguments_renaming.arguments_names sr in
@@ -1103,7 +1096,8 @@ let vernac_declare_arguments locality r l nargs flags =
       let sr', impl = List.fold_map (fun b -> function
         | (Anonymous, _,_, true, max), Name id -> assert false
         | (Name x, _,_, true, _), Anonymous ->
-            error ("Argument "^Id.to_string x^" cannot be declared implicit.")
+            errorlabstrm "vernac_declare_arguments"
+              (str "Argument " ++ pr_id x ++ str " cannot be declared implicit.")
         | (Name iid, _,_, true, max), Name id ->
            set_renamed iid id;
            b || not (Id.equal iid id), Some (ExplByName id, max, false)
@@ -1116,8 +1110,12 @@ let vernac_declare_arguments locality r l nargs flags =
       some_renaming_specified l in
   if some_renaming_specified then
     if not (List.mem `Rename flags) then
-      error ("To rename arguments the \"rename\" flag must be specified."
-        ^ pr_renamed_arg ())
+      errorlabstrm "vernac_declare_arguments"
+        (str "To rename arguments the \"rename\" flag must be specified." ++
+           match !renamed_arg with
+           | None -> mt ()
+           | Some (o,n) ->
+              str "\nArgument " ++ pr_id o ++ str " renamed to " ++ pr_id n ++ str ".")
     else
       Arguments_renaming.rename_arguments
         (make_section_locality locality) sr names_decl;
@@ -1581,7 +1579,8 @@ let print_about_hyp_globs ref_or_by_not glnumopt =
       | Some n,AN (Ident (_loc,id)) ->  (* goal number given, catch if wong *)
 	 (try get_nth_goal n,id
 	  with
-	    Failure _ -> Errors.error ("No such goal: "^string_of_int n^"."))
+	    Failure _ -> errorlabstrm "print_about_hyp_globs"
+                           (str "No such goal: " ++ int n ++ str "."))
       | _ , _ -> raise NoHyp in
     let hyps = pf_hyps gl in
     let (id,bdyopt,typ) = Context.lookup_named id hyps in
@@ -1674,8 +1673,8 @@ let interp_search_about_item env =
 	    (fun _ -> true) s sc in
 	GlobSearchSubPattern (Pattern.PRef ref)
       with UserError _ ->
-	error ("Unable to interp \""^s^"\" either as a reference or \
-          	as an identifier component")
+	errorlabstrm "interp_search_about_item"
+          (str "Unable to interp \"" ++ str s ++ str "\" either as a reference or as an identifier component")
 
 let vernac_search s gopt r =
   let r = interp_search_restriction r in
-- 
cgit v1.2.3


From 2e3835560ce221f8e4686062502ab24ae63a388d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 25 Apr 2015 10:09:11 +0200
Subject: Cleaning some uses of exceptions in tactics.

---
 tactics/tactics.ml | 12 ++++--------
 1 file changed, 4 insertions(+), 8 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8117e4131b..6dc219ae6c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1392,9 +1392,8 @@ let descend_in_conjunctions avoid tac exit c =
 		 (* Might be ill-typed due to forbidden elimination. *)
 		 Tacticals.New.onLastHypId (tac (not isrec))]
            end))
-    | None ->
-	raise Exit
-  with RefinerError _|UserError _|Exit -> exit ()
+    | None -> exit ()
+  with RefinerError _|UserError _ -> exit ()
   end
 
 (****************************************************)
@@ -1473,15 +1472,12 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind))
                 let info = Loc.add_loc info loc in
 		Proofview.tclZERO ~info exn0 in
             if not (Int.equal concl_nprod 0) then
-              try
                 Proofview.tclORELSE
                   (try_apply thm_ty 0)
                   (function (e, info) -> match e with
                   | PretypeError _|RefinerError _|UserError _|Failure _->
                     tac
                   | exn -> iraise (exn, info))
-              with UserError _ | Exit ->
-                tac
             else
               tac
 	in try_red_apply thm_ty0
@@ -1596,10 +1592,10 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
             tac id
           ])
     with e when with_destruct && Errors.noncritical e ->
-      let e = Errors.push e in
+      let (e, info) = Errors.push e in
         (descend_in_conjunctions [targetid]
            (fun b id -> aux (id::idstoclear) b (mkVar id))
-           (fun _ -> iraise e) c)
+           (fun _ -> Proofview.tclZERO ~info e) c)
     end
   in
   aux [] with_destruct d
-- 
cgit v1.2.3


From 3cf7a09799982924453df29b3bb4d081a0e089b4 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sun, 26 Apr 2015 21:51:49 +0200
Subject: Open the file chooser even if there is no current session. (Fix bug
 #4206)

---
 ide/coqide.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 0f4cb7b073..c0e2281258 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -253,14 +253,14 @@ let newfile _ =
   !refresh_editor_hook ();
   notebook#goto_page index
 
-let load sn =
-  let filename = sn.fileops#filename in
+let load _ =
+  let filename =
+    try notebook#current_term.fileops#filename
+    with Invalid_argument _ -> None in
   match select_file_for_open ~title:"Load file" ?filename () with
     | None -> ()
     | Some f -> FileAux.load_file f
 
-let load = cb_on_current_term load
-
 let save _ = on_current_term (FileAux.check_save ~saveas:false)
 
 let saveas sn =
-- 
cgit v1.2.3


From 62b0708ebfda01e377c4e6e229be4388a96cbecc Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 27 Apr 2015 11:21:35 +0200
Subject: Fix some ill-typed debugging code in the VM.

---
 kernel/byterun/coq_interp.c | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 0ab9f89ffa..ddbde9d385 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -77,9 +77,11 @@ sp is a local copy of the global variable extern_sp. */
 #ifdef _COQ_DEBUG_ 
 #   define print_instr(s) /*if (drawinstr)*/ printf("%s\n",s)
 #   define print_int(i)   /*if (drawinstr)*/ printf("%d\n",i)
+#   define print_lint(i)  /*if (drawinstr)*/ printf("%ld\n",i)
 # else 
 #   define print_instr(s) 
 #   define print_int(i) 
+#   define print_lint(i)
 #endif
 
 /* GC interface */
@@ -795,12 +797,12 @@ value coq_interprete
 	if (Is_block(accu)) {
 	  long index = Tag_val(accu);
 	  print_instr("block");
-	  print_int(index);
+	  print_lint(index);
 	  pc += pc[(sizes & 0xFFFFFF) + index];
 	} else {
 	  long index = Long_val(accu);
 	  print_instr("constant");
-	  print_int(index);
+	  print_lint(index);
 	  pc += pc[index];
 	}
 	  Next;
@@ -957,7 +959,7 @@ value coq_interprete
 	    sp -= nargs;
 	    for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2);
 	    *--sp = accu;
-	    print_int(nargs);
+	    print_lint(nargs);
 	    coq_extra_args = nargs;
 	    pc = Code_val(coq_env);
 	    goto check_stacks;
-- 
cgit v1.2.3


From 2887393cf817d0509caf7a2bb8f7850e2bc2d123 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 27 Apr 2015 12:07:36 +0200
Subject: Compile the VM code with some optimizations (+130% speedup).

Option -g has no impact on the code generated by GCC, so it is now
systematically added, since it is quite helpful when the VM segfaults
(e.g. bug #4203). Note that, even for a debug build, option -O1 is
preferred to -O0, since -O0 produces assembly code that is much too noisy
for debugging.

For non-debugging builds, -O2 was chosen rather than -O3, since it led to
a noticeably faster VM. I guess even recent GCC compilers still have a
hard time optimizing humongous functions such as the VM.

Here are the results on a simple benchmark: computing the factorial of a
large number with Z and BigZ. (Factorial of 2*6! for Z, of 7! for BigZ.)
For comparison purpose, the timings of native_compute are also provided.

      Z     BigZ
-O0   6.4   12.3
-O1   4.3   10.7
-O2   2.8    7.3
-O3   3.0    9.3
n_c   2.0    2.4
---
 configure.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/configure.ml b/configure.ml
index 92d71813c1..68fe7e1211 100644
--- a/configure.ml
+++ b/configure.ml
@@ -396,8 +396,7 @@ let coq_annotate_flag =
   then if program_in_path "ocamlmerlin" then "-bin-annot" else "-dtypes"
   else ""
 
-let cflags = "-Wall -Wno-unused"
-
+let cflags = "-Wall -Wno-unused -g " ^ (if !Prefs.debug then "-O1" else "-O2")
 
 (** * Architecture *)
 
-- 
cgit v1.2.3


From 5fc6e3a9e8fdd81be83194bbd62093993ddd4b01 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 27 Apr 2015 23:03:41 +0200
Subject: Improve syntax highlighting.

- Arithmetic operators and brackets are no longer recognized as bullets,
  unless they follow a stop or start a line.
- Most vernacular commands are no longer highlighted when used inside
  proof scripts.
- Coqdoc comments now take precedence over regular comments.
---
 ide/coq.lang | 360 ++++++++++++++++++++++++++++++-----------------------------
 1 file changed, 186 insertions(+), 174 deletions(-)

diff --git a/ide/coq.lang b/ide/coq.lang
index 65150d6a95..35dff85e62 100644
--- a/ide/coq.lang
+++ b/ide/coq.lang
@@ -5,7 +5,7 @@
     <property name="block-comment-start">\(\*</property>
     <property name="block-comment-stop">\*\)</property>
   </metadata>
-  
+
   <styles>
     <style id="comment" _name="Comment" map-to="def:comment"/>
     <style id="coqdoc" _name="Coqdoc text" map-to="def:note"/>
@@ -20,15 +20,15 @@
     <style id="safe" _name="Checked Part"/>
     <style id="sentence" _name="Sentence terminator"/>
   </styles>
-  
+
   <definitions>
     <define-regex id="space">\s+</define-regex>
     <define-regex id="first_ident_char">[_\p{L}]</define-regex>
     <define-regex id="ident_char">[_\p{L}'\pN]</define-regex>
     <define-regex id="ident">\%{first_ident_char}\%{ident_char}*</define-regex>
     <define-regex id="qualit">(\%{ident}\.)*\%{ident}</define-regex>
-    <define-regex id="undotted_sep">[-+*{}]</define-regex>
     <define-regex id="dot_sep">\.(\s|\z)</define-regex>
+    <define-regex id="bullet">([-+*]+|{)(\s|\z)|}(\s*})*</define-regex>
     <define-regex id="single_decl">Definition|Let|Example|SubClass|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|Record|Structure|Ltac|Instance|Class|Existing\%{space}Instance|Canonical\%{space}Structure|Coercion</define-regex>
     <define-regex id="mult_decl">Hypothes[ie]s|Axiom(s)?|Variable(s)?|Parameter(s)?|Context|Implicit\%{space}Type(s)?</define-regex>
     <define-regex id="locality">((Local|Global)\%{space})?</define-regex>
@@ -36,185 +36,197 @@
     <define-regex id="end_proof">Qed|Defined|Admitted|Abort|Save</define-regex>
     <define-regex id="decl_head">((?'gal'\%{locality}(Program\%{space})?(\%{single_decl}|\%{begin_proof}))\%{space}(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}\%{ident})*))|(?'gal2'Goal)</define-regex>
 
-    <context id="escape-seq" style-ref="escape">
-      <match>""</match>
-    </context>
-    <context id="string" style-ref="string">
+    <!-- Strings, with '""' an escape sequence -->
+    <context id="string" style-ref="string" class="string">
       <start>"</start>
       <end>"</end>
       <include>
-	<context ref="escape-seq"/>
+        <context id="string-escape" style-ref="escape">
+          <match>""</match>
+        </context>
+      </include>
+    </context>
+
+    <!-- Coqdoc comments -->
+    <context id="coqdoc" style-ref="coqdoc" class="comment" class-disabled="no-spell-check">
+      <start>\(\*\*(\s|\z)</start>
+      <end>\*\)</end>
+      <include>
+        <context ref="comment"/>
+        <context ref="string"/>
+        <context ref="def:in-comment"/>
       </include>
     </context>
+
+    <!-- Regular comments, possibly nested -->
+    <context id="comment" style-ref="comment" class="comment" class-disabled="no-spell-check">
+      <start>\(\*</start>
+      <end>\*\)</end>
+      <include>
+        <context ref="comment"/>
+        <context ref="string"/>
+        <context ref="def:in-comment"/>
+      </include>
+    </context>
+
+    <!-- Keywords for constr -->
+    <context id="constr-keyword" style-ref="constr-keyword">
+      <keyword>forall</keyword>
+      <keyword>fun</keyword>
+      <keyword>match</keyword>
+      <keyword>fix</keyword>
+      <keyword>cofix</keyword>
+      <keyword>with</keyword>
+      <keyword>for</keyword>
+      <keyword>end</keyword>
+      <keyword>as</keyword>
+      <keyword>let</keyword>
+      <keyword>in</keyword>
+      <keyword>if</keyword>
+      <keyword>then</keyword>
+      <keyword>else</keyword>
+      <keyword>return</keyword>
+    </context>
+
+    <!-- Sort keywords -->
+    <context id="constr-sort" style-ref="constr-sort">
+      <keyword>Prop</keyword>
+      <keyword>Set</keyword>
+      <keyword>Type</keyword>
+    </context>
+
     <context id="coq" class="no-spell-check">
       <include>
         <context ref="string"/>
-	<context id="coqdoc" style-ref="coqdoc" class-disabled="no-spell-check">
-	  <start>\(\*\*(\s|\z)</start>
-	  <end>\*\)</end>
-	  <include>
-	    <context ref="comment-in-comment"/>
-	    <context ref="string"/>
-	  </include>
-	</context>
-	<context id="comment" style-ref="comment" class="comment" class-disabled="no-spell-check">
-	  <start>\(\*</start>
-	  <end>\*\)</end>
-	  <include>
-	    <context id="comment-in-comment" style-ref="comment" class="comment" class-disabled="no-spell-check">
-	      <start>\(\*</start>
-	      <end>\*\)</end>
-	      <include>
-		<context ref="comment-in-comment"/>
-		<context ref="string"/>
-	      </include>
-	    </context>
-	    <context ref="string"/>
-	  </include>
-	</context>
-	<context id="declaration">
-	  <start>\%{decl_head}</start>
-	  <end>\%{dot_sep}</end>
-	  <include>
-	    <context sub-pattern="id" where="start" style-ref="identifier"/>
-	    <context sub-pattern="gal" where="start" style-ref="gallina-keyword"/>
-	    <context sub-pattern="gal2" where="start" style-ref="gallina-keyword"/>
-	    <context sub-pattern="id_list" where="start" style-ref="identifier"/>
-	    <context sub-pattern="gal4list" where="start" style-ref="gallina-keyword"/>
-	    <context id="constr-keyword" style-ref="constr-keyword">
-	      <keyword>forall</keyword>
-	      <keyword>fun</keyword>
-	      <keyword>match</keyword>
-	      <keyword>fix</keyword>
-	      <keyword>cofix</keyword>
-	      <keyword>with</keyword>
-	      <keyword>for</keyword>
-	      <keyword>end</keyword>
-	      <keyword>as</keyword>
-	      <keyword>let</keyword>
-	      <keyword>in</keyword>
-	      <keyword>if</keyword>
-	      <keyword>then</keyword>
-	      <keyword>else</keyword>
-	      <keyword>return</keyword>
-	    </context>
-	    <context id="constr-sort" style-ref="constr-sort">
-	      <keyword>Prop</keyword>
-	      <keyword>Set</keyword>
-	      <keyword>Type</keyword>
-	    </context>
-	    <context id="dot-nosep">
-	      <match>\.\.</match>
-	    </context>
-	    <context ref="comment"/>
-	    <context ref="string"/>
-	    <context ref="coqdoc"/>
-	  </include>
-	</context>
-	<context id="proof">
-	  <start>Proof(\%{dot_sep}|\%{space}using|\%{space}with)</start>
-	  <end>\%{end_proof}\%{dot_sep}</end>
-	  <include>
-	    <context sub-pattern="0" where="start" style-ref="vernac-keyword"/>
-	    <context sub-pattern="0" where="end" style-ref="vernac-keyword"/>
-	    <context ref="command"/>
-	    <context ref="scope-command"/>
-	    <context ref="hint-command"/>
-	    <context ref="command-for-qualit"/>
-	    <context ref="declaration"/>
-	    <context ref="comment"/>
-	    <context ref="string"/>
-	    <context ref="coqdoc"/>
-	    <context ref="proof"/>
-	    <context ref="undotted-sep"/>
-	    <context id="tactic" extend-parent="false">
-	      <start>\b[^-+*{}]</start>
-	      <end>\%{dot_sep}</end>
-	      <include>
-		<context ref="dot-nosep"/>
-		<context ref="constr-keyword"/>
-		<context ref="constr-sort"/>
-	      </include>
-	    </context>
-	  </include>
-	</context>
-	<context id="exact-proof">
-	  <start>Proof</start>
-	  <end>\%{dot_sep}</end>
-	  <include>
-	    <context sub-pattern="0" where="start" style-ref="vernac-keyword"/>
-	    <context ref="constr-keyword"/>
-	    <context ref="constr-sort"/>
-	  </include>
-	</context>
-	<context id="undotted-sep" style-ref="vernac-keyword">
-	  <match>\%{undotted_sep}</match>
-	</context>
-	<context id="command" style-ref="vernac-keyword">
-	  <keyword>Add</keyword>
-	  <keyword>Check</keyword>
-	  <keyword>Eval</keyword>
-	  <keyword>Load</keyword>
-	  <keyword>Undo</keyword>
-	  <keyword>(Print|Reset)\%{space}+Extraction\%{space}+(Inline|Blacklist)</keyword>
-	  <keyword>Print</keyword>
-	  <keyword>Comments</keyword>
-	  <keyword>Solve\%{space}Obligation</keyword>
-	  <keyword>(Uns|S)et(\%{space}\%{ident})+</keyword>
-	  <keyword>(\%{locality}|(Reserved|Tactic)\%{space})?Notation</keyword>
-	  <keyword>\%{locality}Infix</keyword>
-	  <keyword>Declare\%{space}ML\%{space}Module</keyword>
-	  <keyword>Extraction\%{space}Language\%{space}(Ocaml|Haskell|Scheme|JSON)</keyword>
-	</context>
-	<context id="hint-command" style-ref="vernac-keyword">
-	  <prefix>\%{locality}Hint\%{space}</prefix>
-	  <keyword>Resolve</keyword>
-	  <keyword>Immediate</keyword>
-	  <keyword>Constructors</keyword>
-	  <keyword>Unfold</keyword>
-	  <keyword>Opaque</keyword>
-	  <keyword>Transparent</keyword>
-	  <keyword>Extern</keyword>
-	  <keyword>Rewrite</keyword>
-	</context>
-	<context id="scope-command" style-ref="vernac-keyword">
-	  <suffix>\%{space}Scope</suffix>
-	  <keyword>\%{locality}Open</keyword>
-	  <keyword>\%{locality}Close</keyword>
-	  <keyword>Bind</keyword>
-	  <keyword>Delimit</keyword>
-	</context>
-	<context id="command-for-qualit">
-	  <suffix>\%{space}(?'qua'\%{qualit})</suffix>
-	  <keyword>Chapter</keyword>
-	  <keyword>Combined\%{space}Scheme</keyword>
-	  <keyword>Scheme\%{space}(Induction|Minimality|Elimination|Case|Equality)\%{space}for</keyword>
-	  <keyword>End</keyword>
-	  <keyword>Section</keyword>
-	  <keyword>Module(\%{space}Type)?</keyword>
-	  <keyword>Declare\%{space}Module(\%{space}(Import|Export))?</keyword>
-	  <keyword>About</keyword>
-	  <keyword>Arguments</keyword>
-	  <keyword>Implicit\%{space}Arguments</keyword>
-	  <keyword>Include</keyword>
-	  <keyword>Extract\%{space}((Inlined\%{space})?Constant|Inductive)</keyword>
-	  <include>
-	    <context sub-pattern="1" style-ref="vernac-keyword"/>
-	    <context sub-pattern="qua" style-ref="identifier"/>
-	  </include>
-	</context>
-	<context id="command-for-qualit-list">
-	  <suffix>(?'qua_list'(\%{space}\%{qualit})+)</suffix>
-	  <keyword>Typeclasses (Transparent|Opaque)</keyword>
-	  <keyword>Require(\%{space}(Import|Export))?</keyword>
-	  <keyword>Import</keyword>
-	  <keyword>Export</keyword>
-	  <keyword>((Recursive|Separate)\%{space})?Extraction(\%{space}(Library|(No)?Inline|Blacklist))?</keyword>
-	  <include>
-	    <context sub-pattern="1" style-ref="vernac-keyword"/>
-	    <context sub-pattern="qua_list" style-ref="identifier"/>
-	  </include>
-	</context>
+        <context ref="coqdoc"/>
+        <context ref="comment"/>
+
+        <context id="declaration">
+          <start>\%{decl_head}</start>
+          <end>\%{dot_sep}</end>
+          <include>
+            <context sub-pattern="id" where="start" style-ref="identifier"/>
+            <context sub-pattern="gal" where="start" style-ref="gallina-keyword"/>
+            <context sub-pattern="gal2" where="start" style-ref="gallina-keyword"/>
+            <context sub-pattern="id_list" where="start" style-ref="identifier"/>
+            <context sub-pattern="gal4list" where="start" style-ref="gallina-keyword"/>
+            <context ref="constr-keyword"/>
+            <context ref="constr-sort"/>
+            <context id="dot-nosep">
+              <match>\.\.</match>
+            </context>
+            <context ref="string"/>
+            <context ref="coqdoc"/>
+            <context ref="comment"/>
+          </include>
+        </context>
+
+        <context id="proof">
+          <start>Proof(\%{dot_sep}|\%{space}using|\%{space}with)</start>
+          <end>\%{end_proof}\%{dot_sep}</end>
+          <include>
+            <context sub-pattern="0" where="start" style-ref="vernac-keyword"/>
+            <context sub-pattern="0" where="end" style-ref="vernac-keyword"/>
+            <context ref="command-in-proof"/>
+            <context ref="string"/>
+            <context ref="coqdoc"/>
+            <context ref="comment"/>
+            <context ref="constr-keyword"/>
+            <context ref="constr-sort"/>
+            <context id="bullet" extend-parent="false">
+              <match>\%{dot_sep}\s*(?'bul'\%{bullet})</match>
+              <include>
+                <context sub-pattern="bul" style-ref="vernac-keyword"/>
+              </include>
+            </context>
+            <context id="bullet-sol" style-ref="vernac-keyword">
+              <match>^\s*\%{bullet}</match>
+            </context>
+          </include>
+        </context>
+
+        <context id="exact-proof">
+          <start>Proof</start>
+          <end>\%{dot_sep}</end>
+          <include>
+            <context sub-pattern="0" where="start" style-ref="vernac-keyword"/>
+            <context ref="constr-keyword"/>
+            <context ref="constr-sort"/>
+          </include>
+        </context>
+
+        <context id="command-in-proof" style-ref="vernac-keyword">
+          <keyword>About</keyword>
+          <keyword>Check</keyword>
+          <keyword>Print</keyword>
+          <keyword>Eval</keyword>
+          <keyword>Undo</keyword>
+          <keyword>Opaque</keyword>
+          <keyword>Transparent</keyword>
+        </context>
+
+        <context id="command" style-ref="vernac-keyword">
+          <keyword>Add</keyword>
+          <keyword>Load</keyword>
+          <keyword>(Print|Reset)\%{space}+Extraction\%{space}+(Inline|Blacklist)</keyword>
+          <keyword>Comments</keyword>
+          <keyword>Solve\%{space}Obligation</keyword>
+          <keyword>(Uns|S)et(\%{space}\%{ident})+</keyword>
+          <keyword>(\%{locality}|(Reserved|Tactic)\%{space})?Notation</keyword>
+          <keyword>\%{locality}Infix</keyword>
+          <keyword>Declare\%{space}ML\%{space}Module</keyword>
+          <keyword>Extraction\%{space}Language\%{space}(Ocaml|Haskell|Scheme|JSON)</keyword>
+        </context>
+
+        <context id="hint-command" style-ref="vernac-keyword">
+          <prefix>\%{locality}Hint\%{space}</prefix>
+          <keyword>Resolve</keyword>
+          <keyword>Immediate</keyword>
+          <keyword>Constructors</keyword>
+          <keyword>Unfold</keyword>
+          <keyword>Extern</keyword>
+          <keyword>Rewrite</keyword>
+        </context>
+
+        <context id="scope-command" style-ref="vernac-keyword">
+          <suffix>\%{space}Scope</suffix>
+          <keyword>\%{locality}Open</keyword>
+          <keyword>\%{locality}Close</keyword>
+          <keyword>Bind</keyword>
+          <keyword>Delimit</keyword>
+        </context>
+
+        <context id="command-for-qualit">
+          <suffix>\%{space}(?'qua'\%{qualit})</suffix>
+          <keyword>Chapter</keyword>
+          <keyword>Combined\%{space}Scheme</keyword>
+          <keyword>Scheme\%{space}(Induction|Minimality|Elimination|Case|Equality)\%{space}for</keyword>
+          <keyword>End</keyword>
+          <keyword>Section</keyword>
+          <keyword>Module(\%{space}Type)?</keyword>
+          <keyword>Declare\%{space}Module(\%{space}(Import|Export))?</keyword>
+          <keyword>Arguments</keyword>
+          <keyword>Implicit\%{space}Arguments</keyword>
+          <keyword>Include</keyword>
+          <keyword>Extract\%{space}((Inlined\%{space})?Constant|Inductive)</keyword>
+          <include>
+            <context sub-pattern="1" style-ref="vernac-keyword"/>
+            <context sub-pattern="qua" style-ref="identifier"/>
+          </include>
+        </context>
+
+        <context id="command-for-qualit-list">
+          <suffix>(?'qua_list'(\%{space}\%{qualit})+)</suffix>
+          <keyword>Typeclasses (Transparent|Opaque)</keyword>
+          <keyword>Require(\%{space}(Import|Export))?</keyword>
+          <keyword>Import</keyword>
+          <keyword>Export</keyword>
+          <keyword>((Recursive|Separate)\%{space})?Extraction(\%{space}(Library|(No)?Inline|Blacklist))?</keyword>
+          <include>
+            <context sub-pattern="1" style-ref="vernac-keyword"/>
+            <context sub-pattern="qua_list" style-ref="identifier"/>
+          </include>
+        </context>
       </include>
     </context>
   </definitions>
-- 
cgit v1.2.3


From 857e82b2ca0d164242070599b66138cc431509c9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 1 May 2015 10:21:36 +0200
Subject: Giving to "subst" a more natural semantic (fixing #4214) by using all
 equalities in configurations like

x=y
x=z
===
P(x,y,z)

where it now produces

===
P(z,z,z)

In particular (equations are processed from most ancient to most recent).

Thanks to this, a "repeat subst" can just be a "subst" in List.v.

Incidentally: moved a nf_enter to enter in subst_one, since the latter
is normally called from other tactics having normalized evars.
---
 tactics/equality.ml           | 61 +++++++++++++++++++++++++++++--------------
 test-suite/bugs/closed/4214.v |  5 ++++
 theories/Lists/List.v         |  2 +-
 3 files changed, 47 insertions(+), 21 deletions(-)
 create mode 100644 test-suite/bugs/closed/4214.v

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 5d6fcc5b10..f2860a2300 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1589,10 +1589,10 @@ let is_eq_x gl x (id,_,c) =
    erase hyp and x; proceed by generalizing all dep hyps *)
 
 let subst_one dep_proof_ok x (hyp,rhs,dir) =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
-  let hyps = Proofview.Goal.hyps gl in
-  let concl = Proofview.Goal.concl gl in
+  let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
+  let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
   (* The set of hypotheses using x *)
   let dephyps =
     List.rev (snd (List.fold_right (fun (id,b,_ as dcl) (deps,allhyps) ->
@@ -1663,24 +1663,45 @@ let default_subst_tactic_flags () =
     { only_leibniz = true; rewrite_dependent_proof = false }
 
 let subst_all ?(flags=default_subst_tactic_flags ()) () =
-  Proofview.Goal.nf_enter begin fun gl ->
-  let find_eq_data_decompose = find_eq_data_decompose gl in
-  let test (_,c) =
-    try
-      let lbeq,u,(_,x,y) = find_eq_data_decompose c in
-      let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
-      if flags.only_leibniz then restrict_to_eq_and_identity eq;
-      (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
-      if Term.eq_constr x y then failwith "caught";
-      match kind_of_term x with Var x -> x | _ ->
-      match kind_of_term y with Var y -> y | _ -> failwith "caught"
-    with Constr_matching.PatternMatchingFailure -> failwith "caught"
+
+  (* First step: find hypotheses to treat in linear time *)
+  let find_equations gl =
+    let gl = Proofview.Goal.assume gl in
+    let find_eq_data_decompose = find_eq_data_decompose gl in
+    let test (hyp,_,c) =
+      try
+        let lbeq,u,(_,x,y) = find_eq_data_decompose c in
+        let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
+        if flags.only_leibniz then restrict_to_eq_and_identity eq;
+        (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
+        if Term.eq_constr x y then None else
+        match kind_of_term x, kind_of_term y with
+        | Var _, _ | _, Var _ -> Some hyp
+        | _ -> None
+      with Constr_matching.PatternMatchingFailure -> None
+    in
+    let hyps = Proofview.Goal.hyps gl in
+    List.map_filter test hyps
+  in
+
+  (* Second step: treat equations *)
+  let process hyp =
+    Proofview.Goal.enter begin fun gl ->
+    let gl = Proofview.Goal.assume gl in
+    let find_eq_data_decompose = find_eq_data_decompose gl in
+    let (_,_,c) = pf_get_hyp hyp gl in
+    let _,_,(_,x,y) = find_eq_data_decompose c in
+    (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
+    if Term.eq_constr x y then Proofview.tclUNIT () else
+      match kind_of_term x, kind_of_term y with
+      | Var x, _ -> subst_one flags.rewrite_dependent_proof x (hyp,y,true)
+      | _, Var y -> subst_one flags.rewrite_dependent_proof y (hyp,x,false)
+      | _ -> Proofview.tclUNIT ()
+    end
   in
-  let test p = try Some (test p) with Failure _ -> None in
-  let hyps = pf_hyps_types gl in
-  let ids = List.map_filter test hyps in
-  let ids = List.uniquize ids in
-  subst_gen flags.rewrite_dependent_proof ids
+  Proofview.Goal.nf_enter begin fun gl ->
+    let ids = find_equations gl in
+    tclMAP process ids
   end
 
 (* Rewrite the first assumption for which a condition holds
diff --git a/test-suite/bugs/closed/4214.v b/test-suite/bugs/closed/4214.v
new file mode 100644
index 0000000000..cd53c898e9
--- /dev/null
+++ b/test-suite/bugs/closed/4214.v
@@ -0,0 +1,5 @@
+(* Check that subst uses all equations around *)
+Goal forall A (a b c : A), b = a -> b = c -> a = c.
+intros.
+subst.
+reflexivity.
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index ea07a8497a..5819fbe5ef 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -2202,7 +2202,7 @@ Section ForallPairs.
   Proof.
     induction 1.
     inversion 1.
-    simpl; destruct 1; destruct 1; repeat subst; auto.
+    simpl; destruct 1; destruct 1; subst; auto.
     right; left. apply -> Forall_forall; eauto.
     right; right. apply -> Forall_forall; eauto.
   Qed.
-- 
cgit v1.2.3


From f19d0c7baf91fb410de77baed391b0a16db9c4e2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 1 May 2015 11:33:59 +0200
Subject: Fixing computation of implicit arguments by position in fixpoints
 (#4217).

---
 interp/constrintern.ml        | 8 ++++----
 interp/constrintern.mli       | 2 +-
 test-suite/bugs/closed/4217.v | 6 ++++++
 toplevel/command.ml           | 2 +-
 4 files changed, 12 insertions(+), 6 deletions(-)
 create mode 100644 test-suite/bugs/closed/4217.v

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 8f0d56c5bd..982d9bfe39 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1893,7 +1893,7 @@ let intern_context global_level env impl_env binders =
   with InternalizationError (loc,e) ->
     user_err_loc (loc,"internalize", explain_internalization_error e)
 
-let interp_rawcontext_evars env evdref bl =
+let interp_rawcontext_evars env evdref k bl =
   let (env, par, _, impls) =
     List.fold_left
       (fun (env,params,n,impls) (na, k, b, t) ->
@@ -1914,11 +1914,11 @@ let interp_rawcontext_evars env evdref bl =
 	      let c = understand_judgment_tcc env evdref b in
 	      let d = (na, Some c.uj_val, c.uj_type) in
 		(push_rel d env, d::params, n, impls))
-      (env,[],1,[]) (List.rev bl)
+      (env,[],k+1,[]) (List.rev bl)
   in (env, par), impls
 
-let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) env evdref params =
+let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env evdref params =
   let int_env,bl = intern_context global_level env impl_env params in
-  let x = interp_rawcontext_evars env evdref bl in
+  let x = interp_rawcontext_evars env evdref shift bl in
   int_env, x
 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 0d33d43345..4d2c994679 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -157,7 +157,7 @@ val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> types
 (** Interpret contexts: returns extended env and context *)
 
 val interp_context_evars :
-  ?global_level:bool -> ?impl_env:internalization_env ->
+  ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int ->
   env -> evar_map ref -> local_binder list ->
   internalization_env * ((env * rel_context) * Impargs.manual_implicits)
 
diff --git a/test-suite/bugs/closed/4217.v b/test-suite/bugs/closed/4217.v
new file mode 100644
index 0000000000..19973f30a7
--- /dev/null
+++ b/test-suite/bugs/closed/4217.v
@@ -0,0 +1,6 @@
+(* Checking correct index of implicit by pos in fixpoints *)
+
+Fixpoint ith_default
+         {default_A : nat}
+         {As : list nat}
+         {struct As} : Set.
diff --git a/toplevel/command.ml b/toplevel/command.ml
index cdeecf1bb7..1249581eec 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -733,7 +733,7 @@ type structured_fixpoint_expr = {
 let interp_fix_context env evdref isfix fix =
   let before, after = if isfix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in
   let impl_env, ((env', ctx), imps) = interp_context_evars env evdref before in
-  let impl_env', ((env'', ctx'), imps') = interp_context_evars ~impl_env env' evdref after in
+  let impl_env', ((env'', ctx'), imps') = interp_context_evars ~impl_env ~shift:(List.length before) env' evdref after in
   let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in
     ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot)
 
-- 
cgit v1.2.3


From 2a295131a1a72dd56e6e7abdeaeca07b1b69ab6d Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel
Date: Thu, 23 Apr 2015 01:14:49 -0400
Subject: Add a [Redirect] vernacular command

The command [Redirect "filename" (...)] redirects all the output of
[(...)]  to file "filename.out". This is useful for storing the results of
an [Eval compute], for redirecting the results of a large search, for
automatically generating traces of interesting developments, and so on.
---
 doc/refman/RefMan-oth.tex |  3 +++
 intf/vernacexpr.mli       |  1 +
 lib/pp.ml                 | 21 +++++++++++++++++++++
 lib/pp.mli                |  2 ++
 parsing/g_vernac.ml4      |  1 +
 printing/ppvernac.ml      |  2 ++
 stm/stm.ml                |  4 ++--
 stm/texmacspp.ml          |  3 +++
 stm/vernac_classifier.ml  |  2 +-
 toplevel/vernac.ml        |  2 +-
 toplevel/vernacentries.ml |  3 +++
 11 files changed, 40 insertions(+), 4 deletions(-)

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 0a28a93a41..aa0291a23f 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -877,6 +877,9 @@ go();;
 This command executes the vernacular command \textrm{\textsl{command}}
 and display the time needed to execute it.
 
+\subsection[\tt Time \textrm{\textsl{command}}.]{\tt Redirect "\textrm{\textsl{file}}" \textrm{\textsl{command}}.\comindex{Redirect}
+\label{redirect}}
+This command executes the vernacular command \textrm{\textsl{command}}, redirecting its output to ``\textrm{\textsl{file}}.out''.
 
 \subsection[\tt Timeout \textrm{\textsl{int}} \textrm{\textsl{command}}.]{\tt Timeout \textrm{\textsl{int}} \textrm{\textsl{command}}.\comindex{Timeout}
 \label{timeout}}
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 450b1af0f9..d7b269a1de 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -273,6 +273,7 @@ type vernac_expr =
   (* Control *)
   | VernacLoad of verbose_flag * string
   | VernacTime of vernac_list
+  | VernacRedirect of string * vernac_list
   | VernacTimeout of int * vernac_expr
   | VernacFail of vernac_expr
   | VernacError of exn (* always fails *)
diff --git a/lib/pp.ml b/lib/pp.ml
index 9667f7270e..30bc30a9ad 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -448,6 +448,27 @@ let logger = ref std_logger
 let make_pp_emacs() = print_emacs:=true; logger:=emacs_logger
 let make_pp_nonemacs() = print_emacs:=false; logger := std_logger
 
+let ft_logger old_logger ft ~id level mesg = match level with
+  | Debug _ -> msgnl_with ft (debugbody mesg)
+  | Info -> msgnl_with ft (infobody mesg)
+  | Notice -> msgnl_with ft mesg
+  | Warning -> old_logger ~id:id level mesg
+  | Error -> old_logger ~id:id level mesg
+
+let with_output_to_file fname func input =
+  let old_logger = !logger in
+  let channel = open_out (String.concat "." [fname; "out"]) in
+  logger := ft_logger old_logger (Format.formatter_of_out_channel channel);
+  try
+    let output = func input in
+    logger := old_logger;
+    close_out channel;
+    output
+  with reraise ->
+    let reraise = Backtrace.add_backtrace reraise in
+    logger := old_logger;
+    close_out channel;
+    Exninfo.iraise reraise
 
 let feedback_id = ref (Feedback.Edit 0)
 let feedback_route = ref Feedback.default_route
diff --git a/lib/pp.mli b/lib/pp.mli
index e20e5ca82a..3b1123a9dc 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -12,6 +12,8 @@
 val make_pp_emacs:unit -> unit
 val make_pp_nonemacs:unit -> unit
 
+val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
+
 (** Pretty-printers. *)
 
 type std_ppcmds
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index cf7f6af28b..09059b410e 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -79,6 +79,7 @@ GEXTEND Gram
   GLOBAL: vernac gallina_ext tactic_mode noedit_mode subprf subgoal_command;
   vernac: FIRST
     [ [ IDENT "Time"; l = vernac_list -> VernacTime l
+      | IDENT "Redirect"; s = ne_string; l = vernac_list -> VernacRedirect (s, l)
       | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v)
       | IDENT "Fail"; v = vernac -> VernacFail v
 
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index c6b1b672f8..832c08fe0e 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -627,6 +627,8 @@ module Make
           )
         | VernacTime v ->
           return (keyword "Time" ++ spc() ++ pr_vernac_list v)
+        | VernacRedirect (s, v) ->
+          return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_list v)
         | VernacTimeout(n,v) ->
           return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac v)
         | VernacFail v ->
diff --git a/stm/stm.ml b/stm/stm.ml
index f36b757f29..9771564752 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -86,7 +86,7 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } =
     | VernacResetName _ | VernacResetInitial | VernacBack _
     | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
     | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true
-    | VernacTime el -> List.for_all (fun (_,e) -> internal_command e) el
+    | VernacTime el | VernacRedirect (_,el) -> List.for_all (fun (_,e) -> internal_command e) el
     | _ -> false in
   if internal_command expr then begin
     prerr_endline ("ignoring " ^ string_of_ppcmds(pr_vernac expr))
@@ -1472,7 +1472,7 @@ end = struct (* {{{ *)
     let e, etac, time, fail =
       let rec find time fail = function
         | VernacSolve(_,_,re,b) -> re, b, time, fail
-        | VernacTime [_,e] -> find true fail e
+        | VernacTime [_,e] | VernacRedirect (_,[_,e]) -> find true fail e
         | VernacFail e -> find time true e
         | _ -> errorlabstrm "Stm" (str"unsupported") in find false false e in
     Hooks.call Hooks.with_fail fail (fun () ->
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index 180f20ae81..9edc1f1c70 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -490,6 +490,9 @@ let rec tmpp v loc =
   | VernacTime l ->
       xmlApply loc (Element("time",[],[]) ::
                     List.map (fun(loc,e) ->tmpp e loc) l)
+  | VernacRedirect (s, l) ->
+      xmlApply loc (Element("redirect",["path", s],[]) ::
+                      List.map (fun(loc,e) ->tmpp e loc) l)
   | VernacTimeout (s,e) ->
       xmlApply loc (Element("timeout",["val",string_of_int s],[]) ::
                     [tmpp e loc])
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 783ff2e116..2b5eb86834 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -86,7 +86,7 @@ let rec classify_vernac e =
 	make_polymorphic (classify_vernac e)
       else classify_vernac e
     | VernacTimeout (_,e) -> classify_vernac e
-    | VernacTime e -> classify_vernac_list e
+    | VernacTime e | VernacRedirect (_, e) -> classify_vernac_list e
     | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
         (match classify_vernac e with
         | ( VtQuery _ | VtProofStep _ | VtSideff _
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index b3694d0e98..11cb047e09 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -27,7 +27,7 @@ let rec is_navigation_vernac = function
   | VernacBacktrack _
   | VernacBackTo _
   | VernacBack _ -> true
-  | VernacTime l ->
+  | VernacRedirect (_, l) | VernacTime l ->
     List.exists
       (fun (_,c) -> is_navigation_vernac c) l (* Time Back* is harmless *)
   | c -> is_deep_navigation_vernac c
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f33c71d8a6..4300d5e244 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1849,6 +1849,7 @@ let interp ?proof locality poly c =
   | VernacLoad _ -> assert false
   | VernacFail _ -> assert false
   | VernacTime _ -> assert false
+  | VernacRedirect _ -> assert false
   | VernacTimeout _ -> assert false
   | VernacStm _ -> assert false
 
@@ -2127,6 +2128,8 @@ let interp ?(verbosely=true) ?proof (loc,c) =
     | VernacTimeout (n,v) ->
         current_timeout := Some n;
         aux ?locality ?polymorphism isprogcmd v
+    | VernacRedirect (s, v) ->
+         Pp.with_output_to_file s (aux_list ?locality ?polymorphism isprogcmd) v;
     | VernacTime v ->
         System.with_time !Flags.time
           (aux_list ?locality ?polymorphism isprogcmd) v;
-- 
cgit v1.2.3


From 5d504553a068e97ec4ac01b0ddbc251d7dfc1ea3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 4 May 2015 15:07:33 +0200
Subject: Fix documentation of Redirect

---
 CHANGES                   | 8 ++++++++
 doc/refman/RefMan-oth.tex | 2 +-
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/CHANGES b/CHANGES
index b1dffde147..87506dadc1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,11 @@
+Changes from V8.5beta2 to ...
+===================================
+
+Vernacular commands
+
+- New command "Redirect" to redirect the output of a command to a file.
+
+
 Changes from V8.5beta1 to V8.5beta2
 ===================================
 
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index aa0291a23f..739a89af4c 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -877,7 +877,7 @@ go();;
 This command executes the vernacular command \textrm{\textsl{command}}
 and display the time needed to execute it.
 
-\subsection[\tt Time \textrm{\textsl{command}}.]{\tt Redirect "\textrm{\textsl{file}}" \textrm{\textsl{command}}.\comindex{Redirect}
+\subsection[\tt Redirect "\textrm{\textsl{file}}" \textrm{\textsl{command}}.]{\tt Redirect "\textrm{\textsl{file}}" \textrm{\textsl{command}}.\comindex{Redirect}
 \label{redirect}}
 This command executes the vernacular command \textrm{\textsl{command}}, redirecting its output to ``\textrm{\textsl{file}}.out''.
 
-- 
cgit v1.2.3


From df54c829a4c06a93de47df4e8ccc441721360da8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 25 Apr 2015 13:31:17 +0200
Subject: Code simplification in Tactics.

---
 tactics/tactics.ml | 95 +++++++++++++++++++++++++++++-------------------------
 1 file changed, 51 insertions(+), 44 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6dc219ae6c..3038a95068 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1358,7 +1358,7 @@ let make_projection env sigma params cstr sign elim i n c u =
       | None -> None
   in elim
 
-let descend_in_conjunctions avoid tac exit c =
+let descend_in_conjunctions avoid tac (err, info) c =
   Proofview.Goal.nf_enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
@@ -1392,8 +1392,8 @@ let descend_in_conjunctions avoid tac exit c =
 		 (* Might be ill-typed due to forbidden elimination. *)
 		 Tacticals.New.onLastHypId (tac (not isrec))]
            end))
-    | None -> exit ()
-  with RefinerError _|UserError _ -> exit ()
+    | None -> Proofview.tclZERO ~info err
+  with RefinerError _|UserError _ -> Proofview.tclZERO ~info err
   end
 
 (****************************************************)
@@ -1416,7 +1416,15 @@ let solve_remaining_apply_goals =
     with Not_found -> Proofview.tclUNIT ()
   else Proofview.tclUNIT ()
   end
-  
+
+let tclORELSEOPT t k =
+  Proofview.tclORELSE t
+    (fun e -> match k e with
+    | None ->
+      let (e, info) = e in
+      Proofview.tclZERO ~info e
+    | Some tac -> tac)
+
 let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) =
   Proofview.Goal.nf_enter begin fun gl ->
   let concl = Proofview.Goal.concl gl in
@@ -1441,47 +1449,46 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind))
       with UserError _ as exn ->
         Proofview.tclZERO exn
     in
-    Proofview.tclORELSE
+    let rec try_red_apply thm_ty (exn0, info) =
+      try
+        (* Try to head-reduce the conclusion of the theorem *)
+        let red_thm = try_red_product env sigma thm_ty in
+        tclORELSEOPT
+          (try_apply red_thm concl_nprod)
+          (function (e, info) -> match e with
+          | PretypeError _|RefinerError _|UserError _|Failure _ ->
+            Some (try_red_apply red_thm (exn0, info))
+          | _ -> None)
+      with Redelimination ->
+        (* Last chance: if the head is a variable, apply may try
+            second order unification *)
+        let info = Loc.add_loc info loc in
+        let tac =
+          if with_destruct then
+            descend_in_conjunctions []
+              (fun b id ->
+                Tacticals.New.tclTHEN
+                  (try_main_apply b (mkVar id))
+                  (Proofview.V82.tactic (thin [id])))
+              (exn0, info) c
+          else
+            Proofview.tclZERO ~info exn0 in
+        if not (Int.equal concl_nprod 0) then
+          tclORELSEOPT
+            (try_apply thm_ty 0)
+            (function (e, info) -> match e with
+            | PretypeError _|RefinerError _|UserError _|Failure _->
+              Some tac
+            | _ -> None)
+        else
+          tac
+    in
+    tclORELSEOPT
       (try_apply thm_ty0 concl_nprod)
       (function (e, info) -> match e with
-        | PretypeError _|RefinerError _|UserError _|Failure _ as exn0 ->
-	let rec try_red_apply thm_ty =
-          try 
-            (* Try to head-reduce the conclusion of the theorem *)
-            let red_thm = try_red_product env sigma thm_ty in
-            Proofview.tclORELSE
-              (try_apply red_thm concl_nprod)
-              (function (e, info) -> match e with
-              | PretypeError _|RefinerError _|UserError _|Failure _ ->
-		try_red_apply red_thm
-              | exn -> iraise (exn, info))
-          with Redelimination ->
-            (* Last chance: if the head is a variable, apply may try
-	       second order unification *)
-            let tac =
-	      if with_destruct then
-                descend_in_conjunctions []
-                  (fun b id ->
-                    Tacticals.New.tclTHEN
-                      (try_main_apply b (mkVar id))
-                      (Proofview.V82.tactic (thin [id])))
-                  (fun _ ->
-                    let info = Loc.add_loc info loc in
-                    Proofview.tclZERO ~info exn0) c
-	      else
-                let info = Loc.add_loc info loc in
-		Proofview.tclZERO ~info exn0 in
-            if not (Int.equal concl_nprod 0) then
-                Proofview.tclORELSE
-                  (try_apply thm_ty 0)
-                  (function (e, info) -> match e with
-                  | PretypeError _|RefinerError _|UserError _|Failure _->
-                    tac
-                  | exn -> iraise (exn, info))
-            else
-              tac
-	in try_red_apply thm_ty0
-      | exn -> iraise (exn, info))
+      | PretypeError _|RefinerError _|UserError _|Failure _ ->
+        Some (try_red_apply thm_ty0 (e, info))
+      | _ -> None)
     end
   in
     Tacticals.New.tclTHENLIST [
@@ -1595,7 +1602,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
       let (e, info) = Errors.push e in
         (descend_in_conjunctions [targetid]
            (fun b id -> aux (id::idstoclear) b (mkVar id))
-           (fun _ -> Proofview.tclZERO ~info e) c)
+           (e, info) c)
     end
   in
   aux [] with_destruct d
-- 
cgit v1.2.3