From bb3c3713929ff8647004c18faaebcc311335cfa9 Mon Sep 17 00:00:00 2001
From: Pierre Boutillier
Date: Tue, 3 Feb 2015 22:01:17 +0100
Subject: Hardcode how coqide have to look for coqtop in MacOS bundle

Sorry, that is ugly. Please revert if you see a better way to do it.
---
 ide/ideutils.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index a869442696..84ef8f40db 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -243,7 +243,14 @@ let coqtop_path () =
 	    let i = Str.search_backward (Str.regexp_string "coqide") prog pos
             in
 	    String.blit "coqtop" 0 prog i 6;
-	    if Sys.file_exists prog then prog else "coqtop"
+	    if Sys.file_exists prog then prog
+	    else
+	      let in_macos_bundle =
+		Filename.concat
+		  (Filename.dirname prog)
+		  (Filename.concat "../Resources/bin" (Filename.basename prog))
+	      in if Sys.file_exists in_macos_bundle then in_macos_bundle
+		 else "coqtop"
 	  with Not_found -> "coqtop"
   in file
 
-- 
cgit v1.2.3


From 997230709aed2b1d2f57f9ac8829991fa01e9b5c Mon Sep 17 00:00:00 2001
From: Pierre Boutillier
Date: Tue, 3 Feb 2015 23:12:56 +0100
Subject: Fixup version & copyright for MacOS bundle

---
 Makefile.build                | 2 +-
 configure.ml                  | 3 ++-
 ide/MacOS/Info.plist.template | 2 +-
 3 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/Makefile.build b/Makefile.build
index 0d87d98e96..c3936c1a7a 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -388,7 +388,7 @@ install-ide-info:
 $(COQIDEAPP)/Contents:
 	rm -rdf $@
 	$(MKDIR) $@
-	sed -e "s/VERSION/$(VERSION)/g" ide/MacOS/Info.plist.template > $@/Info.plist
+	sed -e "s/VERSION/$(VERSION4MACOS)/g" ide/MacOS/Info.plist.template > $@/Info.plist
 	$(MKDIR) "$@/MacOS"
 
 $(COQIDEINAPP): ide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents
diff --git a/configure.ml b/configure.ml
index 0c1d39127f..6d30b28312 100644
--- a/configure.ml
+++ b/configure.ml
@@ -1124,7 +1124,8 @@ let write_makefile f =
   List.iter (fun (v,msg,_,_) -> pr "# %s: path for %s\n" v msg) install_dirs;
   List.iter (fun (v,_,dir,_) -> pr "%s=%S\n" v dir) install_dirs;
   pr "\n# Coq version\n";
-  pr "VERSION=%s\n\n" coq_version;
+  pr "VERSION=%s\n" coq_version;
+  pr "VERSION4MACOS=%s\n\n" coq_macos_version;
   pr "# Objective-Caml compile command\n";
   pr "OCAML=%S\n" camlexec.top;
   pr "OCAMLC=%S\n" camlexec.byte;
diff --git a/ide/MacOS/Info.plist.template b/ide/MacOS/Info.plist.template
index fd80c83969..e224e81204 100644
--- a/ide/MacOS/Info.plist.template
+++ b/ide/MacOS/Info.plist.template
@@ -66,7 +66,7 @@
 	<key>CFBundleGetInfoString</key>
 	<string>Coq_vVERSION</string>
 	<key>NSHumanReadableCopyright</key>
-	<string>Copyright 1999-2014, The Coq Development Team INRIA - CNRS - LIX - LRI - PPS</string>
+	<string>Copyright 1999-2015, The Coq Development Team INRIA - CNRS - LIX - LRI - PPS</string>
 	<key>CFBundleHelpBookFolder</key>
 	<string>share/doc/coq/html/</string>
 	<key>CFAppleHelpAnchor</key>
-- 
cgit v1.2.3


From 7dc6dfee7eb641282f4268aea24c688da07470ee Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 13 Feb 2015 20:13:33 +0100
Subject: Document the issue with trivial inductive types. (Workaround for bug
 #3984)

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

diff --git a/CHANGES b/CHANGES
index ca31ca2398..7f134679fc 100644
--- a/CHANGES
+++ b/CHANGES
@@ -22,6 +22,10 @@ Logic
   the return predicate. Restores compatibility of Coq's logic with the
   propositional extensionality axiom. May create incompatibilities in
   recursive programs heavily using dependent types.
+- Trivial inductive types are no longer defined in Type but in Prop, which
+  leads to a non-dependent induction principle being generated in place of
+  the dependent one. To recover the old behavior, explicitly define your
+  inductive types in Set.
 
 Vernacular commands
 
-- 
cgit v1.2.3


From ea083ac106f048e64c1b57ddd37ac717236b8ecd Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 14 Feb 2015 12:54:36 +0100
Subject: Univs: When computing the level of an inductive including indices,
 lets do not contribute. Fixes bug #3808.

---
 kernel/indtypes.ml            | 10 ++++++----
 test-suite/bugs/closed/3808.v |  2 ++
 2 files changed, 8 insertions(+), 4 deletions(-)
 create mode 100644 test-suite/bugs/closed/3808.v

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index ea575e1e0d..799471c68a 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -164,10 +164,12 @@ let infer_constructor_packet env_ar_par ctx params lc =
 (* If indices matter *)
 let cumulate_arity_large_levels env sign =
   fst (List.fold_right
-    (fun (_,_,t as d) (lev,env) ->
-      let tj = infer_type env t in
-      let u = univ_of_sort tj.utj_type in
-	(Universe.sup u lev, push_rel d env))
+    (fun (_,b,t as d) (lev,env) ->
+      if Option.is_empty b then
+	let tj = infer_type env t in
+	let u = univ_of_sort tj.utj_type in
+	  (Universe.sup u lev, push_rel d env)
+      else lev, push_rel d env)
     sign (Universe.type0m,env))
 
 let is_impredicative env u =
diff --git a/test-suite/bugs/closed/3808.v b/test-suite/bugs/closed/3808.v
new file mode 100644
index 0000000000..6e19ddf8dc
--- /dev/null
+++ b/test-suite/bugs/closed/3808.v
@@ -0,0 +1,2 @@
+Inductive Foo : (let enforce := (fun x => x) : Type@{j} -> Type@{i} in Type@{i})
+  := foo : Foo.
\ No newline at end of file
-- 
cgit v1.2.3


From 40072e20736198485fa5381c6af4dd8c87a077da Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 14 Feb 2015 13:32:29 +0100
Subject: Univs: fix bug #3755. We were missing refreshements of universes in
 unifications ?X ~= ?Y foo not catched by solve_evar_evar.

---
 pretyping/evarsolve.ml        | 28 +++++++++-------------------
 test-suite/bugs/closed/3755.v | 16 ++++++++++++++++
 2 files changed, 25 insertions(+), 19 deletions(-)
 create mode 100644 test-suite/bugs/closed/3755.v

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 921609aae3..adfe9dd8de 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -64,30 +64,33 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
     in
       modified := true; evdref := evd; mkSort s'
     | Prod (na,u,v) -> 
-    mkProd (na,u,refresh dir v)
+      mkProd (na,u,refresh dir v)
     | _ -> t
   (** Refresh the types of evars under template polymorphic references *)
-  and refresh_term_evars onevars t =
+  and refresh_term_evars onevars top t =
     match kind_of_term t with
     | App (f, args) when is_template_polymorphic env f ->
       let pos = get_polymorphic_positions f in
 	refresh_polymorphic_positions args pos
+    | App (f, args) when top && isEvar f -> 
+      refresh_term_evars true false f; 
+      Array.iter (refresh_term_evars onevars false) args
     | Evar (ev, a) when onevars ->
       let evi = Evd.find !evdref ev in
       let ty' = refresh true evi.evar_concl in
 	if !modified then 
 	  evdref := Evd.add !evdref ev {evi with evar_concl = ty'}
 	else ()
-    | _ -> iter_constr (refresh_term_evars onevars) t
+    | _ -> iter_constr (refresh_term_evars onevars false) t
   and refresh_polymorphic_positions args pos =
     let rec aux i = function
       | Some l :: ls -> 
         if i < Array.length args then 
-	  ignore(refresh_term_evars true args.(i));
+	  ignore(refresh_term_evars true false args.(i));
         aux (succ i) ls
       | None :: ls -> 
         if i < Array.length args then 
-          ignore(refresh_term_evars false args.(i));
+          ignore(refresh_term_evars false false args.(i));
 	aux (succ i) ls
       | [] -> ()
     in aux 0 pos
@@ -97,7 +100,7 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
       (match pbty with
       | None -> t
       | Some dir -> refresh dir t)
-    else (refresh_term_evars false t; t)
+    else (refresh_term_evars false true t; t)
   in
     if !modified then !evdref, t' else !evdref, t
 
@@ -1385,19 +1388,6 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
             map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
               imitate envk t in
 
-  let _fast rhs = 
-    let filter_ctxt = evar_filtered_context evi in
-    let names = ref Idset.empty in
-    let rec is_id_subst ctxt s =
-       match ctxt, s with
-         | ((id, _, _) :: ctxt'), (c :: s') ->
-           names := Idset.add id !names;
-           isVarId id c && is_id_subst ctxt' s'
-         | [], [] -> true
-         | _ -> false in
-    is_id_subst filter_ctxt (Array.to_list argsv) &&
-    closed0 rhs &&
-    Idset.subset (collect_vars rhs) !names in
   let rhs = whd_beta evd rhs (* heuristic *) in
   let fast rhs = 
     let filter_ctxt = evar_filtered_context evi in
diff --git a/test-suite/bugs/closed/3755.v b/test-suite/bugs/closed/3755.v
new file mode 100644
index 0000000000..77427ace58
--- /dev/null
+++ b/test-suite/bugs/closed/3755.v
@@ -0,0 +1,16 @@
+(* File reduced by coq-bug-finder from original input, then from 6729 lines to 
+411 lines, then from 148 lines to 115 lines, then from 99 lines to 70 lines, 
+then from 85 lines to 63 lines, then from 76 lines to 55 lines, then from 61 
+lines to 17 lines *)
+(* coqc version trunk (January 2015) compiled on Jan 17 2015 21:58:5 with OCaml 
+4.01.0
+   coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk 
+(9e6b28c04ad98369a012faf3bd4d630cf123a473) *)
+Set Printing Universes.
+Section param.
+  Variable typeD : Set -> Set.
+  Variable STex : forall (T : Type) (p : T -> Set), Set.
+  Definition existsEach_cons' v (P : @sigT _ typeD -> Set) :=
+    @STex _ (fun x => P (@existT _ _ v x)).
+
+  Check @existT _ _ STex STex.
-- 
cgit v1.2.3


From 01f0c21c6d45d44b1fc78f1a41ea1cb8d1b550f0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 14 Feb 2015 14:54:37 +0100
Subject: coqc accepts -top option. Fixes bug #4043.

---
 tools/coqc.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/coqc.ml b/tools/coqc.ml
index 5c7be41bec..7e822dbe36 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -121,7 +121,7 @@ let parse_args () =
     | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir"
       |"-load-vernac-source"|"-l"|"-load-vernac-object"
       |"-load-ml-source"|"-require"|"-load-ml-object"
-      |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"
+      |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top"
       |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs"
       as o) :: rem ->
 	begin
-- 
cgit v1.2.3


From bc77234dc5d40d4540793ceead1595b15ab18bb8 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 14 Feb 2015 15:11:29 +0100
Subject: dependent destruction: Fix (part of) bug #3961, by fixing dependent *
 generalizing * which was broken since 8.4.

---
 doc/refman/RefMan-tacex.tex | 18 +++++++++++++-----
 theories/Program/Equality.v | 11 +++++++++--
 2 files changed, 22 insertions(+), 7 deletions(-)

diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex
index 668a68c9c7..9f4ddc8044 100644
--- a/doc/refman/RefMan-tacex.tex
+++ b/doc/refman/RefMan-tacex.tex
@@ -247,7 +247,7 @@ to simplify equalities appearing at the beginning of induction
 hypotheses, generally using trivial applications of
 reflexivity. In cases where the equality is not between constructor
 forms though, one must help the automation by giving
-some arguments, using the {\tt specialize} tactic.
+some arguments, using the {\tt specialize} tactic for example.
 
 \begin{coq_example*}
 destruct D... apply weak ; apply ax. apply ax.
@@ -257,16 +257,24 @@ destruct D...
 Show.
 \end{coq_example}
 \begin{coq_example}
-  specialize (IHterm G empty).
+  specialize (IHterm G0 empty eq_refl).
 \end{coq_example}
 
-Then the automation can find the needed equality {\tt G = G} to narrow
-the induction hypothesis further. This concludes our example.
+Once the induction hypothesis has been narrowed to the right equality,
+it can be used directly. 
 
 \begin{coq_example}
-  simpl_depind.
+  apply weak, IHterm.
 \end{coq_example}
 
+If there is an easy first-order solution to these equations as in this subgoal, the
+{\tt specialize\_eqs} tactic can be used instead of giving explicit proof
+terms:
+
+\begin{coq_example}
+  specialize_eqs IHterm.
+\end{coq_example}
+This concludes our example.
 \SeeAlso The induction \ref{elim}, case \ref{case} and inversion \ref{inversion} tactics.
 
 \section[\tt autorewrite]{\tt autorewrite\label{autorewrite-example}}
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index a9aa30df5f..ae6fe7dd0a 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -426,8 +426,9 @@ Ltac depind id := do_depind ltac:(fun hyp => do_ind hyp) id.
 (** A variant where generalized variables should be given by the user. *)
 
 Ltac do_depelim' rev tac H :=
-  (try intros until H) ; block_goal ; rev H ;
-  (try revert_until H ; block_goal) ; generalize_eqs H ; tac H ; simpl_dep_elim.
+  (try intros until H) ; block_goal ; 
+  (try revert_until H ; block_goal) ; 
+  generalize_eqs H ; rev H ; tac H ; simpl_dep_elim.
 
 (** Calls [destruct] on the generalized hypothesis, results should be similar to inversion.
    By default, we don't try to generalize the hyp by its variable indices.  *)
@@ -463,3 +464,9 @@ Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) :
 
 Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := 
   do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => induction hyp using c) H.
+
+Tactic Notation "dependent" "induction" ident(H) "in" ne_hyp_list(l) :=
+  do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => induction hyp in l) H.
+
+Tactic Notation "dependent" "induction" ident(H) "in" ne_hyp_list(l) "using" constr(c) := 
+  do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => induction hyp in l using c) H.
-- 
cgit v1.2.3


From 150ef1fa8cf93d7aee765cc878287b79b29c787f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 14 Feb 2015 15:57:49 +0100
Subject: Fixing bug #4016.

When setoid rewriting in a hypothesis, we push the newly introduced declaration
after the last declaration it depends on.
---
 tactics/rewrite.ml | 32 ++++++++++++++++++--------------
 1 file changed, 18 insertions(+), 14 deletions(-)

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 0140f74f50..9289c6d663 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1464,28 +1464,32 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
           in Some proof
       in Some (Some (evars, res, newt))
 
+(** Insert a declaration after the last declaration it depends on *)
+let rec insert_dependent env decl accu hyps = match hyps with
+| [] -> List.rev_append accu [decl]
+| (id, _, _  as ndecl) :: rem ->
+  if occur_var_in_decl env id decl then
+    List.rev_append accu (decl :: hyps)
+  else
+    insert_dependent env decl (ndecl :: accu) rem
+
 let assert_replacing id newt tac = 
   let prf = Proofview.Goal.nf_enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
-    let nc' =
-      Environ.fold_named_context
-        (fun _ (n, b, t as decl) nc' ->
-          if Id.equal n id then (n, b, newt) :: nc'
-          else decl :: nc')
-        env ~init:[]
+    let ctx = Environ.named_context env in
+    let after, before = List.split_when (fun (n, b, t) -> Id.equal n id) ctx in
+    let nc = match before with
+    | [] -> assert false
+    | (id, b, _) :: rem -> insert_dependent env (id, b, newt) [] after @ rem
     in
+    let env' = Environ.reset_with_named_context (val_of_named_context nc) env in
     Proofview.Refine.refine ~unsafe:false begin fun sigma ->
-      let env' = Environ.reset_with_named_context (val_of_named_context nc') env in
       let sigma, ev = Evarutil.new_evar env' sigma concl in
       let sigma, ev' = Evarutil.new_evar env sigma newt in
-      let fold _ (n, b, t) inst =
-        if Id.equal n id then ev' :: inst
-        else mkVar n :: inst
-      in
-      let inst = fold_named_context fold env ~init:[] in
-      let (e, args) = destEvar ev in
-      sigma, mkEvar (e, Array.of_list inst)
+      let map (n, _, _) = if Id.equal n id then ev' else mkVar n in
+      let (e, _) = destEvar ev in
+      sigma, mkEvar (e, Array.map_of_list map nc)
     end
   end in
   Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac)
-- 
cgit v1.2.3


From 93862f2ab93ec3fab3549c868706bc247422674b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 14 Feb 2015 16:09:16 +0100
Subject: Test for bug #4016.

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

diff --git a/test-suite/bugs/closed/4016.v b/test-suite/bugs/closed/4016.v
new file mode 100644
index 0000000000..41cb1a8884
--- /dev/null
+++ b/test-suite/bugs/closed/4016.v
@@ -0,0 +1,12 @@
+Require Import Setoid.
+
+Parameter eq : relation nat.
+Declare Instance Equivalence_eq : Equivalence eq.
+
+Lemma foo : forall z, eq z 0 -> forall x, eq x 0 -> eq z x.
+Proof.
+intros z Hz x Hx.
+rewrite <- Hx in Hz.
+destruct z.
+Abort.
+
-- 
cgit v1.2.3


From 9c5db70b891bf6c3e173a31d4e8761e586c7814a Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sat, 14 Feb 2015 15:09:42 +0100
Subject: Makefile: in byte we can always dynlink

---
 Makefile.common | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/Makefile.common b/Makefile.common
index d752a5be91..e548619610 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -206,6 +206,14 @@ ifneq ($(HASNATDYNLINK),false)
  INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs)
  PLUGINS:=$(PLUGINSCMA)
  PLUGINSOPT:=$(PLUGINSCMA:.cma=.cmxs)
+else
+ifeq ($(BEST),byte)
+ STATICPLUGINS:=
+ INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) \
+	$(FUNINDCMA) $(NATSYNTAXCMA)
+ INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs)
+ PLUGINS:=$(PLUGINSCMA)
+ PLUGINSOPT:=$(PLUGINSCMA:.cma=.cmxs)
 else
  STATICPLUGINS:=$(PLUGINSCMA)
  INITPLUGINS:=
@@ -213,6 +221,7 @@ else
  PLUGINS:=
  PLUGINSOPT:=
 endif
+endif
 
 LINKCMO:=$(CORECMA) $(STATICPLUGINS)
 LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa)
-- 
cgit v1.2.3


From 4a53151f846476f2fbe038a4ecb8e84256a26ba9 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sat, 14 Feb 2015 18:35:04 +0100
Subject: Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior

Of course such proofs cannot be processed asynchronously
---
 COMPATIBILITY                                  |  7 ++++
 doc/refman/RefMan-ltac.tex                     |  8 +++-
 intf/vernacexpr.mli                            |  2 +-
 library/declare.ml                             | 33 ++++++++--------
 library/declare.mli                            |  2 +-
 parsing/g_proofs.ml4                           | 14 ++++---
 plugins/derive/derive.ml                       |  2 +-
 plugins/funind/functional_principles_proofs.ml |  2 +-
 plugins/funind/invfun.ml                       |  2 +-
 plugins/funind/recdef.ml                       |  8 ++--
 printing/ppvernac.ml                           |  9 ++++-
 stm/lemmas.ml                                  | 53 +++++++++++++++++---------
 stm/stm.ml                                     |  7 ++--
 test-suite/success/qed_export.v                | 18 +++++++++
 toplevel/vernacentries.ml                      |  2 +-
 15 files changed, 113 insertions(+), 56 deletions(-)
 create mode 100644 test-suite/success/qed_export.v

diff --git a/COMPATIBILITY b/COMPATIBILITY
index 3b4e8987c9..f23dbad1c5 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -33,6 +33,13 @@ Type classes.
   type information and switching to proof mode is no longer available.
   Use { } (without the vertical bars) instead.
 
+Tactic abstract.
+
+- Auxiliary lemmas generated by the abstract tactic are removed from
+  the global environment and inlined in the proof term when a proof
+  is ended with Qed.  The vehavior of 8.4 can be obtained by ending
+  proofs with "Qed export" or "Qed export ident, .., ident".
+
 Potential sources of incompatibilities between Coq V8.3 and V8.4
 ----------------------------------------------------------------
 
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 689ac14254..1704b4d60b 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1010,13 +1010,19 @@ Fail all:let n:= numgoals in guard n=2.
 Reset Initial.
 \end{coq_eval}
 
-\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}
+\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}\comindex{Qed export}
 \index{Tacticals!abstract@{\tt abstract}}}
 
 From the outside ``\texttt{abstract \tacexpr}'' is the same as
 {\tt solve \tacexpr}. Internally it saves an auxiliary lemma called 
 {\ident}\texttt{\_subproof}\textit{n} where {\ident} is the name of the
 current goal and \textit{n} is chosen so that this is a fresh name.
+Such auxiliary lemma is inlined in the final proof term
+unless the proof is ended with ``\texttt{Qed export}''.  In such
+case the lemma is preserved.  The syntax
+``\texttt{Qed export }\ident$_1$\texttt{, ..., }\ident$_n$''
+is also supported.  In such case the system checks that the names given by the
+user actually exist when the proof is ended.
 
 This tactical is useful with tactics such as \texttt{omega} or
 \texttt{discriminate} that generate huge proof terms. With that tool
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 3f2d002c77..07891d0b48 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -135,7 +135,7 @@ type search_restriction =
 
 type rec_flag       = bool (* true = Rec;           false = NoRec          *)
 type verbose_flag   = bool (* true = Verbose;       false = Silent         *)
-type opacity_flag   = bool (* true = Opaque;        false = Transparent    *)
+type opacity_flag   = Opaque of lident list option | Transparent
 type coercion_flag  = bool (* true = AddCoercion    false = NoCoercion     *)
 type instance_flag  = bool option
   (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *)
diff --git a/library/declare.ml b/library/declare.ml
index 7f42a747ed..c3181e4c75 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -253,24 +253,25 @@ let declare_sideff env fix_exn se =
                if Constant.equal c c' then Some (x,kn) else None) inds_consts)
            knl))
 
-let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) =
-  let cd = (* We deal with side effects of non-opaque constants *)
+let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff=false) (cd, kind) =
+  let cd = (* We deal with side effects *)
     match cd with
-    | Entries.DefinitionEntry ({
-      const_entry_opaque = false; const_entry_body = bo } as de)
-    | Entries.DefinitionEntry ({
-      const_entry_polymorphic = true; const_entry_body = bo } as de)
-      ->
-        let _, seff = Future.force bo in
-        if Declareops.side_effects_is_empty seff then cd
-        else begin
-          let seff = Declareops.uniquize_side_effects seff in
-          Declareops.iter_side_effects
-            (declare_sideff (Global.env ()) (Future.fix_exn_of bo)) seff;
-          Entries.DefinitionEntry { de with
-            const_entry_body = Future.chain ~pure:true bo (fun (pt, _) ->
-              pt, Declareops.no_seff) }
+    | Entries.DefinitionEntry de ->
+        if export_seff ||
+           not de.const_entry_opaque ||
+           de.const_entry_polymorphic then
+          let bo = de.const_entry_body in
+          let _, seff = Future.force bo in
+          if Declareops.side_effects_is_empty seff then cd
+          else begin
+            let seff = Declareops.uniquize_side_effects seff in
+            Declareops.iter_side_effects
+              (declare_sideff (Global.env ()) (Future.fix_exn_of bo)) seff;
+            Entries.DefinitionEntry { de with
+              const_entry_body = Future.chain ~pure:true bo (fun (pt, _) ->
+                pt, Declareops.no_seff) }
         end
+        else cd
     | _ -> cd
   in
   let cst = {
diff --git a/library/declare.mli b/library/declare.mli
index 03b66271a2..d8a00db0cf 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -53,7 +53,7 @@ val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types ->
   constr -> definition_entry
 
 val declare_constant :
- ?internal:internal_flag -> ?local:bool -> Id.t -> constant_declaration -> constant
+ ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant
 
 val declare_definition : 
   ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 27f14c7900..b23841ceff 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -52,15 +52,17 @@ GEXTEND Gram
       | IDENT "Existential"; n = natural; c = constr_body ->
 	  VernacSolveExistential (n,c)
       | IDENT "Admitted" -> VernacEndProof Admitted
-      | IDENT "Qed" -> VernacEndProof (Proved (true,None))
-      | IDENT "Save" -> VernacEndProof (Proved (true,None))
+      | IDENT "Qed" -> VernacEndProof (Proved (Opaque None,None))
+      | IDENT "Qed"; IDENT "export"; l = LIST0 identref SEP "," ->
+          VernacEndProof (Proved (Opaque (Some l),None))
+      | IDENT "Save" -> VernacEndProof (Proved (Opaque None,None))
       | IDENT "Save"; tok = thm_token; id = identref ->
-	  VernacEndProof (Proved (true,Some (id,Some tok)))
+	  VernacEndProof (Proved (Opaque None,Some (id,Some tok)))
       | IDENT "Save"; id = identref ->
-	  VernacEndProof (Proved (true,Some (id,None)))
-      | IDENT "Defined" -> VernacEndProof (Proved (false,None))
+	  VernacEndProof (Proved (Opaque None,Some (id,None)))
+      | IDENT "Defined" -> VernacEndProof (Proved (Transparent,None))
       |	IDENT "Defined"; id=identref ->
-	  VernacEndProof (Proved (false,Some (id,None)))
+	  VernacEndProof (Proved (Transparent,Some (id,None)))
       | IDENT "Restart" -> VernacRestart
       | IDENT "Undo" -> VernacUndo 1
       | IDENT "Undo"; n = natural -> VernacUndo n
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 439b1a5c01..711a8aaf09 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -55,7 +55,7 @@ let start_deriving f suchthat lemma =
         | Proved (opaque, None, obj) ->
             match Proof_global.(obj.entries) with
             | [_;f_def;lemma_def] ->
-                opaque , f_def , lemma_def
+                opaque <> Transparent , f_def , lemma_def
             | _ -> assert false
       in
       (** The opacity of [f_def] is adjusted to be [false], as it
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index eb5221fd69..04347537f2 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -989,7 +989,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
   lemma_type
   (Lemmas.mk_hook (fun _ _ -> ()));
   ignore (Pfedit.by (Proofview.V82.tactic prove_replacement));
-  Lemmas.save_proof (Vernacexpr.Proved(false,None))
+  Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None)))
 
 
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 0c7b0a0b08..b9d7e0d909 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1022,7 +1022,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 
 
 
-let do_save () = Lemmas.save_proof (Vernacexpr.Proved(false,None))
+let do_save () = Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None)))
 
 
 (* [derive_correctness make_scheme functional_induction funs graphs] create correctness and completeness
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5558556e2d..b1cbea51c8 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -60,7 +60,7 @@ let declare_fun f_id kind ?(ctx=Univ.UContext.empty) value =
   let ce = definition_entry ~univs:ctx value (*FIXME *) in
     ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
 
-let defined () = Lemmas.save_proof (Vernacexpr.Proved (false,None))
+let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Transparent,None)))
 
 let def_of_const t =
    match (kind_of_term t) with
@@ -1247,9 +1247,9 @@ let build_new_goal_type () =
 let is_opaque_constant c =
   let cb = Global.lookup_constant c in
   match cb.Declarations.const_body with
-    | Declarations.OpaqueDef _ -> true
-    | Declarations.Undef _ -> true
-    | Declarations.Def _ -> false
+    | Declarations.OpaqueDef _ -> Vernacexpr.Opaque None
+    | Declarations.Undef _ -> Vernacexpr.Opaque None
+    | Declarations.Def _ -> Vernacexpr.Transparent
 
 let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal)   =
   (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *)
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index e9e335ec91..e0b94669c2 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -740,9 +740,14 @@ module Make
 
         | VernacEndProof (Proved (opac,o)) -> return (
           match o with
-            | None -> if opac then keyword "Qed" else keyword "Defined"
+            | None -> (match opac with
+                | Transparent -> keyword "Defined"
+                | Opaque None -> keyword "Qed"
+                | Opaque (Some l) ->
+                    keyword "Qed" ++ spc() ++ str"export" ++
+                      prlist_with_sep (fun () -> str", ") pr_lident l)
             | Some (id,th) -> (match th with
-                | None -> (if opac then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id
+                | None -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id
                 | Some tok -> keyword "Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id)
         )
         | VernacExactProof c ->
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index f2e6877989..63c45116a6 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -185,7 +185,7 @@ let look_for_possibly_mutual_statements = function
 
 (* Saving a goal *)
 
-let save id const cstrs do_guard (locality,poly,kind) hook =
+let save ?export_seff id const cstrs do_guard (locality,poly,kind) hook =
   let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
   try
     let const = adjust_guardness_conditions const do_guard in
@@ -200,7 +200,8 @@ let save id const cstrs do_guard (locality,poly,kind) hook =
           | Local | Discharge -> true
           | Global -> false
           in
-          let kn = declare_constant id ~local (DefinitionEntry const, k) in
+          let kn =
+           declare_constant ?export_seff id ~local (DefinitionEntry const, k) in
           (locality, ConstRef kn) in
     definition_message id;
     call_hook (fun exn -> exn) hook l r
@@ -273,25 +274,25 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im
 let save_hook = ref ignore
 let set_save_hook f = save_hook := f
 
-let save_named proof =
+let save_named ?export_seff proof =
   let id,const,cstrs,do_guard,persistence,hook = proof in
-  save id const cstrs do_guard persistence hook
+  save ?export_seff id const cstrs do_guard persistence hook
 
 let check_anonymity id save_ident =
   if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then
     error "This command can only be used for unnamed theorem."
 
 
-let save_anonymous proof save_ident =
+let save_anonymous ?export_seff proof save_ident =
   let id,const,cstrs,do_guard,persistence,hook = proof in
   check_anonymity id save_ident;
-  save save_ident const cstrs do_guard persistence hook
+  save ?export_seff save_ident const cstrs do_guard persistence hook
 
-let save_anonymous_with_strength proof kind save_ident =
+let save_anonymous_with_strength ?export_seff proof kind save_ident =
   let id,const,cstrs,do_guard,_,hook = proof in
   check_anonymity id save_ident;
   (* we consider that non opaque behaves as local for discharge *)
-  save save_ident const cstrs do_guard (Global, const.const_entry_polymorphic, Proof kind) hook
+  save ?export_seff save_ident const cstrs do_guard (Global, const.const_entry_polymorphic, Proof kind) hook
 
 (* Admitted *)
 
@@ -325,34 +326,50 @@ let get_proof proof do_guard hook opacity =
   (** FIXME *)
   id,{const with const_entry_opaque = opacity},cstrs,do_guard,persistence,hook
 
+let check_exist =
+  List.iter (fun (loc,id) ->
+    if not (Nametab.exists_cci (Lib.make_path id)) then
+        user_err_loc (loc,"",pr_id id ++ str " does not exist.")
+  )
+
 let standard_proof_terminator compute_guard hook =
   let open Proof_global in function
   | Admitted ->
       admit hook ();
       Pp.feedback Feedback.AddedAxiom
-  | Proved (is_opaque,idopt,proof) ->
+  | Proved (opaque,idopt,proof) ->
+      let is_opaque, export_seff, exports = match opaque with
+        | Vernacexpr.Transparent -> false, true, []
+        | Vernacexpr.Opaque None -> true, false, []
+        | Vernacexpr.Opaque (Some l) -> true, true, l in
       let proof = get_proof proof compute_guard hook is_opaque in
       begin match idopt with
-      | None -> save_named proof
-      | Some ((_,id),None) -> save_anonymous proof id
+      | None -> save_named ~export_seff proof
+      | Some ((_,id),None) -> save_anonymous ~export_seff proof id
       | Some ((_,id),Some kind) -> 
-          save_anonymous_with_strength proof kind id
-      end
+          save_anonymous_with_strength ~export_seff proof kind id
+      end;
+      check_exist exports
 
 let universe_proof_terminator compute_guard hook =
   let open Proof_global in function
   | Admitted ->
       admit (hook None) ();
       Pp.feedback Feedback.AddedAxiom
-  | Proved (is_opaque,idopt,proof) ->
+  | Proved (opaque,idopt,proof) ->
+      let is_opaque, export_seff, exports = match opaque with
+        | Vernacexpr.Transparent -> false, true, []
+        | Vernacexpr.Opaque None -> true, false, []
+        | Vernacexpr.Opaque (Some l) -> true, true, l in
       let proof = get_proof proof compute_guard 
 	(hook (Some proof.Proof_global.universes)) is_opaque in
       begin match idopt with
-      | None -> save_named proof
-      | Some ((_,id),None) -> save_anonymous proof id
+      | None -> save_named ~export_seff proof
+      | Some ((_,id),None) -> save_anonymous ~export_seff proof id
       | Some ((_,id),Some kind) -> 
-          save_anonymous_with_strength proof kind id
-      end
+          save_anonymous_with_strength ~export_seff proof kind id
+      end;
+      check_exist exports
 
 let start_proof id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
   let terminator = standard_proof_terminator compute_guard hook in
diff --git a/stm/stm.ml b/stm/stm.ml
index 693c673b40..207afd8aee 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1035,7 +1035,7 @@ end = struct (* {{{ *)
         vernac_interp stop
           ~proof:(pobject, terminator)
           { verbose = false; loc;
-            expr = (VernacEndProof (Proved (true,None))) }) in
+            expr = (VernacEndProof (Proved (Opaque None,None))) }) in
       ignore(Future.join checked_proof);
       RespBuiltProof(proof,time)
     with
@@ -1166,7 +1166,7 @@ end = struct (* {{{ *)
       Reach.known_state ~cache:`No start;
       vernac_interp stop ~proof
         { verbose = false; loc;
-          expr = (VernacEndProof (Proved (true,None))) };
+          expr = (VernacEndProof (Proved (Opaque None,None))) };
       Some proof
     with e ->
       let (e, info) = Errors.push e in
@@ -1564,7 +1564,8 @@ let collect_proof keep cur hd brkind id =
    | id :: _ -> Id.to_string id in
  let loc = (snd cur).loc in
  let is_defined = function
-   | _, { expr = VernacEndProof (Proved (false,_)) } -> true
+   | _, { expr = VernacEndProof (Proved ((Transparent|Opaque (Some _)),_)) } ->
+      true
    | _ -> false in
  let proof_using_ast = function
    | Some (_, ({ expr = VernacProof(_,Some _) } as v)) -> Some v
diff --git a/test-suite/success/qed_export.v b/test-suite/success/qed_export.v
new file mode 100644
index 0000000000..ee84cb94e9
--- /dev/null
+++ b/test-suite/success/qed_export.v
@@ -0,0 +1,18 @@
+Lemma a : True.
+Proof.
+assert True as H.
+  abstract (trivial) using exported_seff.
+exact H.
+Fail Qed export a_subproof.
+Qed export exported_seff.
+Check ( exported_seff : True ).
+
+Lemma b : True.
+Proof.
+assert True as H.
+  abstract (trivial) using exported_seff2.
+exact H.
+Qed.
+
+Fail Check ( exported_seff2 : True ).
+
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 7f435ce960..743cfaccdb 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -496,7 +496,7 @@ let vernac_exact_proof c =
   (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
      called only at the begining of a proof. *)
   let status = by (Tactics.New.exact_proof c) in
-  save_proof (Vernacexpr.Proved(true,None));
+  save_proof (Vernacexpr.(Proved(Opaque None,None)));
   if not status then Pp.feedback Feedback.AddedAxiom
 
 let vernac_assumption locality poly (local, kind) l nl =
-- 
cgit v1.2.3


From f5b7f689e6eeeb439346652566f6d841470376f4 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sat, 14 Feb 2015 18:52:11 +0100
Subject: Attempt to be more colorblind friendly in CoqIDE (Close #4024)

---
 ide/preferences.ml  | 36 +++++++++++++++++++++++++++---------
 ide/preferences.mli |  1 +
 ide/tags.ml         | 24 ++++++++++++++++++++----
 ide/tags.mli        | 10 ++++++++++
 4 files changed, 58 insertions(+), 13 deletions(-)

diff --git a/ide/preferences.ml b/ide/preferences.ml
index 25712f951b..9a4fde2f6e 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -144,6 +144,7 @@ type pref =
       mutable processing_color : string;
       mutable processed_color : string;
       mutable error_color : string;
+      mutable error_fg_color : string;
 
       mutable dynamic_word_wrap : bool;
       mutable show_line_number : bool;
@@ -220,10 +221,11 @@ let current = {
     vertical_tabs = false;
     opposite_tabs = false;
 
-    background_color = "cornsilk";
-    processed_color = "light green";
-    processing_color = "light blue";
-    error_color = "#FFCCCC";
+    background_color = Tags.default_color;
+    processed_color = Tags.default_processed_color;
+    processing_color = Tags.default_processing_color;
+    error_color = Tags.default_error_color;
+    error_fg_color = Tags.default_error_fg_color;
 
     dynamic_word_wrap = false;
     show_line_number = false;
@@ -296,6 +298,7 @@ let save_pref () =
     add "processing_color" [p.processing_color] ++
     add "processed_color" [p.processed_color] ++
     add "error_color" [p.error_color] ++
+    add "error_fg_color" [p.error_fg_color] ++
     add "dynamic_word_wrap" [string_of_bool p.dynamic_word_wrap] ++
     add "show_line_number" [string_of_bool p.show_line_number] ++
     add "auto_indent" [string_of_bool p.auto_indent] ++
@@ -382,6 +385,7 @@ let load_pref () =
     set_hd "processing_color" (fun v -> np.processing_color <- v);
     set_hd "processed_color" (fun v -> np.processed_color <- v);
     set_hd "error_color" (fun v -> np.error_color <- v);
+    set_hd "error_fg_color" (fun v -> np.error_fg_color <- v);
     set_bool "dynamic_word_wrap" (fun v -> np.dynamic_word_wrap <- v);
     set_bool "show_line_number" (fun v -> np.show_line_number <- v);
     set_bool "auto_indent" (fun v -> np.auto_indent <- v);
@@ -466,10 +470,15 @@ let configure ?(apply=(fun () -> ())) () =
       ~text:"Background color of errors"
       ~packing:(table#attach ~expand:`X ~left:0 ~top:3) ()
     in
+    let error_fg_label = GMisc.label
+      ~text:"Foreground color of errors"
+      ~packing:(table#attach ~expand:`X ~left:0 ~top:4) ()
+    in
     let () = background_label#set_xalign 0. in
     let () = processed_label#set_xalign 0. in
     let () = processing_label#set_xalign 0. in
     let () = error_label#set_xalign 0. in
+    let () = error_fg_label#set_xalign 0. in
     let background_button = GButton.color_button
       ~color:(Tags.color_of_string (current.background_color))
       ~packing:(table#attach ~left:1 ~top:0) ()
@@ -486,15 +495,19 @@ let configure ?(apply=(fun () -> ())) () =
       ~color:(Tags.get_error_color ())
       ~packing:(table#attach ~left:1 ~top:3) ()
     in
+    let error_fg_button = GButton.color_button
+      ~color:(Tags.get_error_fg_color ())
+      ~packing:(table#attach ~left:1 ~top:4) ()
+    in
     let reset_button = GButton.button
       ~label:"Reset"
       ~packing:box#pack ()
     in
     let reset_cb () =
-      background_button#set_color (Tags.color_of_string "cornsilk");
-      processing_button#set_color (Tags.color_of_string "light blue");
-      processed_button#set_color (Tags.color_of_string "light green");
-      error_button#set_color (Tags.color_of_string "#FFCCCC");
+      background_button#set_color Tags.(color_of_string default_color);
+      processing_button#set_color Tags.(color_of_string default_processing_color);
+      processed_button#set_color Tags.(color_of_string default_processed_color);
+      error_button#set_color Tags.(color_of_string default_error_color);
     in
     let _ = reset_button#connect#clicked ~callback:reset_cb in
     let label = "Color configuration" in
@@ -503,7 +516,12 @@ let configure ?(apply=(fun () -> ())) () =
       current.processing_color <- Tags.string_of_color processing_button#color;
       current.processed_color <- Tags.string_of_color processed_button#color;
       current.error_color <- Tags.string_of_color error_button#color;
-      !refresh_editor_hook ()
+      current.error_fg_color <- Tags.string_of_color error_fg_button#color;
+      !refresh_editor_hook ();
+      Tags.set_processing_color processing_button#color;
+      Tags.set_processed_color processed_button#color;
+      Tags.set_error_color error_button#color;
+      Tags.set_error_fg_color error_fg_button#color
     in
     custom ~label box callback true
   in
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 1b52d20a4c..ab12e4c7ba 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -71,6 +71,7 @@ type pref =
       mutable processing_color : string;
       mutable processed_color : string;
       mutable error_color : string;
+      mutable error_fg_color : string;
 
       mutable dynamic_word_wrap : bool;
       mutable show_line_number : bool;
diff --git a/ide/tags.ml b/ide/tags.ml
index 04ad9a519c..40d5b4ded3 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -13,15 +13,23 @@ let make_tag (tt:GText.tag_table) ~name prop =
   tt#add new_tag#as_tag;
   new_tag
 
-let processed_color = ref "light green"
-let processing_color = ref "light blue"
-let error_color = ref "#FFCCCC"
+(* These work fine for colorblind people too *)
+let default_processed_color = "light green"
+let default_processing_color = "light blue"
+let default_error_color = "#FF3333"
+let default_error_fg_color = "#FF5555"
+let default_color = "cornsilk"
+
+let processed_color = ref default_processed_color
+let processing_color = ref default_processing_color
+let error_color = ref default_error_color
+let error_fg_color = ref default_error_fg_color
 
 module Script =
 struct
   let table = GText.tag_table ()
   let comment = make_tag table ~name:"comment" []
-  let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE ; `FOREGROUND "red"]
+  let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE ; `FOREGROUND !error_fg_color]
   let error_bg = make_tag table ~name:"error_bg" [`BACKGROUND !error_color]
   let to_process = make_tag table ~name:"to_process" [`BACKGROUND !processing_color]
   let processed = make_tag table ~name:"processed" [`BACKGROUND !processed_color]
@@ -94,3 +102,11 @@ let set_error_color clr =
   let s = string_of_color clr in
   error_color := s;
   Script.error_bg#set_property (`BACKGROUND s)
+
+let get_error_fg_color () = color_of_string !error_fg_color
+
+let set_error_fg_color clr =
+  let s = string_of_color clr in
+  error_fg_color := s;
+  Script.error#set_property (`FOREGROUND s)
+
diff --git a/ide/tags.mli b/ide/tags.mli
index 9c3261d66d..e68015c991 100644
--- a/ide/tags.mli
+++ b/ide/tags.mli
@@ -53,3 +53,13 @@ val set_processing_color : Gdk.color -> unit
 
 val get_error_color : unit -> Gdk.color
 val set_error_color : Gdk.color -> unit
+
+val get_error_fg_color : unit -> Gdk.color
+val set_error_fg_color : Gdk.color -> unit
+
+val default_processed_color : string
+val default_processing_color : string
+val default_error_color : string
+val default_error_fg_color : string
+val default_color : string
+
-- 
cgit v1.2.3


From 12a5ccdf1cb69c745aa72dad923349d411682f8d Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sat, 14 Feb 2015 18:59:11 +0100
Subject: typo

---
 COMPATIBILITY | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/COMPATIBILITY b/COMPATIBILITY
index f23dbad1c5..ce57080932 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -37,7 +37,7 @@ Tactic abstract.
 
 - Auxiliary lemmas generated by the abstract tactic are removed from
   the global environment and inlined in the proof term when a proof
-  is ended with Qed.  The vehavior of 8.4 can be obtained by ending
+  is ended with Qed.  The behavior of 8.4 can be obtained by ending
   proofs with "Qed export" or "Qed export ident, .., ident".
 
 Potential sources of incompatibilities between Coq V8.3 and V8.4
-- 
cgit v1.2.3


From 2bea61e8e1ec02906bf63db4142cb26528bb4d76 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sat, 14 Feb 2015 19:00:38 +0100
Subject: CoqIDE: restore old default colors

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

diff --git a/ide/tags.ml b/ide/tags.ml
index 40d5b4ded3..079cf94853 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -16,8 +16,8 @@ let make_tag (tt:GText.tag_table) ~name prop =
 (* These work fine for colorblind people too *)
 let default_processed_color = "light green"
 let default_processing_color = "light blue"
-let default_error_color = "#FF3333"
-let default_error_fg_color = "#FF5555"
+let default_error_color = "#FFCCCC"
+let default_error_fg_color = "red"
 let default_color = "cornsilk"
 
 let processed_color = ref default_processed_color
-- 
cgit v1.2.3


From dbc334fe9e532e2ce1ac7c4754d809ce0152cfde Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 14 Feb 2015 19:56:10 +0100
Subject: Fixing OCaml 3.12 compilation.

---
 plugins/derive/derive.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 711a8aaf09..a77b552e01 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -55,7 +55,7 @@ let start_deriving f suchthat lemma =
         | Proved (opaque, None, obj) ->
             match Proof_global.(obj.entries) with
             | [_;f_def;lemma_def] ->
-                opaque <> Transparent , f_def , lemma_def
+                opaque <> Vernacexpr.Transparent , f_def , lemma_def
             | _ -> assert false
       in
       (** The opacity of [f_def] is adjusted to be [false], as it
-- 
cgit v1.2.3


From dd790577b8acc241201f6863fe3409a2e08b8757 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sat, 14 Feb 2015 21:09:14 +0100
Subject: Win: update README

---
 README.win | 49 +++++++++++++++++--------------------------------
 1 file changed, 17 insertions(+), 32 deletions(-)

diff --git a/README.win b/README.win
index 5027016f54..8302a707f6 100644
--- a/README.win
+++ b/README.win
@@ -8,10 +8,10 @@ INSTALLATION.
 
     The Coq package for Windows comes with an auto-installer. It will
 install Coq binaries and libraries under any directory you specify
-(C:\Program Files\Coq is the default path). It also creates shortcuts
-in the Windows menus. Alternatively, you can launch Coq using coqide.exe
-or coqtop.exe in the bin sub-directory of the installation
-(C:\Program Files\Coq\bin by default).
+(C:\Coq is the default path). It also creates shortcuts
+in the Windows menus.  Binaries, like coqc.exe,
+are in the bin sub-directory of the installation
+(C:\Coq\bin by default).
 
 COMPILATION.
 ============
@@ -20,40 +20,25 @@ COMPILATION.
     distribution. If you really need to recompile under Windows, here
     are some indications:
 
-    1- Install ocaml for Windows (MinGW port).
-       See: http://caml.inria.fr
+    1- Install cygwin and the wget package
+       See: http://cygwin.com
 
-    2- Install a shell environment with at least:
-         - a C compiler (gcc),
-         - the GNU make utility
+    2- Download and unzip in C:\ the SDK for windows
+       See: https://coq.inria.fr/distrib/current/files/
 
-       The Cygwin environment is well suited for compiling Coq
-       (official packages are made using Cygwin) See:
-       http://www.cygwin.com
+    3- From the cygwin prompt type
 
-    3- In order to compile Coqide, you will need the LablGTK library
-       See: http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html
+        . /cygdrive/c/CoqSDK-85-1/environ
 
-       You also need to install the GTK libraries for Windows (see the
-       installation instruction for LablGTK)
+       The first time the script installs the C toolchain.
 
-    4- In a shell window, type successively
+    4- Then Coq can be compiled as follows:
+ 
+        ./configure -local
+        make
 
-        ./configure
-        make world
-        make install
+    5- To build the installer, type:
 
-    5- Though not nescessary, you can find useful:
-         - Windows version of (X)Emacs: it is a powerful environment for
-           developpers with coloured syntax, modes for compilation and debug,
-           and many more. It is free. See: http://www.gnu.org/software.
-         - Windows subversion client (very useful if you have access to the Coq
-           archive).
-
-    Good luck :-)
-
-    Alternatively, it is now possible (and even recommended ...) to build
-    Windows executables of coq from Linux thanks to a mingw cross-compiler.
-    If interested, please contact us for more details.
+        dev/make-installer-win32.sh
 
     The Coq Team.
-- 
cgit v1.2.3


From 5830f5867f36ebf66bc1f4126762f4b1c1444f94 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sun, 15 Feb 2015 13:13:17 +0100
Subject: Document the behavior change of Instance wrt {|...|}. (Fix for bug
 #3749)

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

diff --git a/CHANGES b/CHANGES
index 7f134679fc..dc7cfa90a7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -74,6 +74,9 @@ Vernacular commands
   the execution of the following tactics.
 - "Optimize Heap" command to tell the OCaml runtime to perform a major
   garbage collection step and heap compaction.
+- "Instance" no longer treats the {|...|} syntax specially; it handles it
+  in the same way as other commands, e.g. "Definition". Use the {...}
+  syntax (no pipe symbols) to recover the old behavior.
 
 Specification Language
 
-- 
cgit v1.2.3


From f9c2d5d26a6a8e15549ada1f69d630acfa1a9437 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 15 Feb 2015 13:39:27 +0100
Subject: Fixing test-suite.

---
 test-suite/bugs/closed/4017.v | 2 ++
 test-suite/bugs/closed/4018.v | 2 +-
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/test-suite/bugs/closed/4017.v b/test-suite/bugs/closed/4017.v
index a6f177b496..aa810f4f0e 100644
--- a/test-suite/bugs/closed/4017.v
+++ b/test-suite/bugs/closed/4017.v
@@ -1,3 +1,5 @@
+Set Implicit Arguments.
+
 (* Use of implicit arguments was lost in multiple variable declarations *)
 Variables 
   (A1 : Type)
diff --git a/test-suite/bugs/closed/4018.v b/test-suite/bugs/closed/4018.v
index c3a045943c..8895e09e02 100644
--- a/test-suite/bugs/closed/4018.v
+++ b/test-suite/bugs/closed/4018.v
@@ -1,3 +1,3 @@
 (* Catching PatternMatchingFailure was lost at some point *)
 Goal nat -> True.
-intros [=].
+Fail intros [=].
-- 
cgit v1.2.3


From 4ed609a7351882664acd5b5f1525700e7150ce0e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 15 Feb 2015 13:57:45 +0100
Subject: Fixing bug #3916.

---
 pretyping/tacred.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 1106fefa39..9d6eb31b44 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1211,9 +1211,10 @@ let one_step_reduce env sigma c =
 	       (ci,p,c,lf), stack)
            with Redelimination -> raise NotStepReducible)
       | Fix fix ->
-	  (match reduce_fix (whd_construct_stack env) sigma fix stack with
+	  (try match reduce_fix (whd_construct_stack env) sigma fix stack with
              | Reduced s' -> s'
-	     | NotReducible -> raise NotStepReducible)
+	     | NotReducible -> raise NotStepReducible
+           with Redelimination -> raise NotStepReducible)
       | _ when isEvalRef env x ->
 	  let ref,u = destEvalRefU x in
           (try
-- 
cgit v1.2.3


From 6a844a236ccef9efb2fb6f86ecba8a6a182a4034 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 15 Feb 2015 13:57:36 +0100
Subject: Test for bug #3916.

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

diff --git a/test-suite/bugs/closed/3916.v b/test-suite/bugs/closed/3916.v
new file mode 100644
index 0000000000..55c3a35c3a
--- /dev/null
+++ b/test-suite/bugs/closed/3916.v
@@ -0,0 +1,3 @@
+Require Import List.
+Fail Hint Resolve -> in_map.
+
-- 
cgit v1.2.3


From eec3b87e8cc782cb83ea2eae241129b79c80d496 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 15 Feb 2015 14:07:15 +0100
Subject: Fixing bug #3490.

---
 pretyping/tacred.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 9d6eb31b44..91cd088443 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -189,6 +189,7 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
              if
 	       Array.for_all (noccurn k) tys
 	       && Array.for_all (noccurn (k+nbfix)) bds
+	       && k <= n
 	     then
 	       (k, List.nth labs (k-1))
 	     else
-- 
cgit v1.2.3


From 362b7ef4422b451e621ca8400692de1decb0503d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 15 Feb 2015 14:08:04 +0100
Subject: Test for bug #3490.

---
 test-suite/bugs/closed/3490.v | 27 +++++++++++++++++++++++++++
 test-suite/bugs/opened/3490.v | 27 ---------------------------
 2 files changed, 27 insertions(+), 27 deletions(-)
 create mode 100644 test-suite/bugs/closed/3490.v
 delete mode 100644 test-suite/bugs/opened/3490.v

diff --git a/test-suite/bugs/closed/3490.v b/test-suite/bugs/closed/3490.v
new file mode 100644
index 0000000000..e7a5caa1de
--- /dev/null
+++ b/test-suite/bugs/closed/3490.v
@@ -0,0 +1,27 @@
+Inductive T : Type :=                                                                                        
+| Var : nat -> T                                                                                                 
+| Arr : T -> T -> T.                                                                                             
+
+Inductive Tele : list T -> Type :=                                                                               
+| Tnil  : @Tele nil                                                                                              
+| Tcons : forall ls, forall (t : @Tele ls) (l : T), @Tele (l :: ls). 
+
+Fail Fixpoint TeleD (ls : list T) (t : Tele ls) {struct t}
+   : { x : Type & x -> nat -> Type } :=
+     match t return { x : Type & x -> nat -> Type } with
+       | Tnil => @existT Type (fun x => x -> nat -> Type) unit (fun (_ : unit) (_ : nat) => unit)
+       | Tcons ls t' l =>
+         let (result, get) := TeleD ls t' in
+         @existT Type (fun x => x -> nat -> Type)
+                 { v : result & (fix TD (t : T) {struct t} :=
+                                   match  t with
+                                     | Var n =>
+                                       get v n
+                                     | Arr a b => TD a -> TD b
+                                   end) l }
+                 (fun x n =>
+                    match n return Type with
+                      | 0 => projT2 x
+                      | S n => get (projT1 x) n
+                    end)
+     end.
diff --git a/test-suite/bugs/opened/3490.v b/test-suite/bugs/opened/3490.v
deleted file mode 100644
index e7a5caa1de..0000000000
--- a/test-suite/bugs/opened/3490.v
+++ /dev/null
@@ -1,27 +0,0 @@
-Inductive T : Type :=                                                                                        
-| Var : nat -> T                                                                                                 
-| Arr : T -> T -> T.                                                                                             
-
-Inductive Tele : list T -> Type :=                                                                               
-| Tnil  : @Tele nil                                                                                              
-| Tcons : forall ls, forall (t : @Tele ls) (l : T), @Tele (l :: ls). 
-
-Fail Fixpoint TeleD (ls : list T) (t : Tele ls) {struct t}
-   : { x : Type & x -> nat -> Type } :=
-     match t return { x : Type & x -> nat -> Type } with
-       | Tnil => @existT Type (fun x => x -> nat -> Type) unit (fun (_ : unit) (_ : nat) => unit)
-       | Tcons ls t' l =>
-         let (result, get) := TeleD ls t' in
-         @existT Type (fun x => x -> nat -> Type)
-                 { v : result & (fix TD (t : T) {struct t} :=
-                                   match  t with
-                                     | Var n =>
-                                       get v n
-                                     | Arr a b => TD a -> TD b
-                                   end) l }
-                 (fun x n =>
-                    match n return Type with
-                      | 0 => projT2 x
-                      | S n => get (projT1 x) n
-                    end)
-     end.
-- 
cgit v1.2.3


From 8cee2c7ef9e15937fafe60ae43fec7c8bb3678c6 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sun, 15 Feb 2015 16:59:37 +0100
Subject: Note about "Undo. Undo." in CHANGES

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

diff --git a/CHANGES b/CHANGES
index dc7cfa90a7..8b4a4fc933 100644
--- a/CHANGES
+++ b/CHANGES
@@ -63,6 +63,8 @@ Vernacular commands
   retrieved using the "Locate Term" command.
 - New "Derive" command to help writing program by derivation.
 - "Undo" undoes any command, not just tactics.
+- "Undo. Undo." does not work in CoqIDE or Proof General, it works only
+  in coqtop.  "Undo 2" should be used intead.
 - New "Refine Instance Mode" option that allows to deactivate the generation of
   obligations in incomplete typeclass instances, raising an error instead.
 - "Collection" command to name sets of section hypotheses.  Named collections
-- 
cgit v1.2.3


From dbb6de3b51dad3c055cb7638fbd6a29df9a6a22d Mon Sep 17 00:00:00 2001
From: Pierre Boutillier
Date: Sat, 14 Feb 2015 16:10:56 +0100
Subject: Fix 'don't expose cases' in cbn

---
 pretyping/reductionops.ml | 9 ++++++++-
 pretyping/tacred.ml       | 7 -------
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index a23963abca..6059e9ff84 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -842,7 +842,14 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
 		    let (tm',sk'),cst_l' =
 		      whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, app_sk)
 		    in
-		      if equal_stacks (x, app_sk) (tm', sk') || Stack.will_expose_iota sk'
+		    let rec is_case x = match kind_of_term x with
+		      | Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x
+		      | App (hd, _) -> is_case hd
+		      | Case _ -> true
+		      | _ -> false in
+		    if equal_stacks (x, app_sk) (tm', sk')
+		       || Stack.will_expose_iota sk'
+		       || is_case tm'
 		      then fold ()
 		      else whrec cst_l' (tm', sk' @ sk)
 		  else match recargs with
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 91cd088443..372b26aa25 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -597,13 +597,6 @@ let reduce_proj env sigma whfun whfun' c =
     | _ -> raise Redelimination
   in redrec c
 
-
-let dont_expose_case = function
-  | EvalVar _ | EvalRel _ | EvalEvar _ -> false
-  | EvalConst c ->
-     Option.cata (fun (_,_,z) -> List.mem `ReductionDontExposeCase z)
-		 false (ReductionBehaviour.get (ConstRef c))
-
 let whd_nothing_for_iota env sigma s =
   let rec whrec (x, stack as s) =
     match kind_of_term x with
-- 
cgit v1.2.3


From aed3c876d422f4dcc0296fd4949148c697f37b1d Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sun, 15 Feb 2015 18:13:04 +0100
Subject: Fix test-suite file. Check that definitions do work when sharing is
 disabled in the kernel.

---
 test-suite/bugs/closed/3309.v | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/test-suite/bugs/closed/3309.v b/test-suite/bugs/closed/3309.v
index 9e12b990b7..049589325e 100644
--- a/test-suite/bugs/closed/3309.v
+++ b/test-suite/bugs/closed/3309.v
@@ -315,8 +315,6 @@ Definition abmonoidfracrel ( X : abmonoid ) ( A : @submonoids X ) :  hrel (@setq
 intros; exact (@quotrel _ _).
 Defined.
 
-(* Unset Kernel Term Sharing. *)
-
 Fail Timeout 1 Axiom ispartlbinopabmonoidfracrel : forall ( X : abmonoid ) ( A : @subabmonoids X ) { L : hrel X } ( z : abmonoidfrac X A ) , @abmonoidfracrel X A ( ( admit + z ) )admit.
 
 Definition ispartlbinopabmonoidfracrel_type : Type :=
@@ -326,3 +324,10 @@ Definition ispartlbinopabmonoidfracrel_type : Type :=
 Fail Timeout 1 Axiom ispartlbinopabmonoidfracrel' : $(let t:= eval unfold ispartlbinopabmonoidfracrel_type in
                                       ispartlbinopabmonoidfracrel_type in exact t)$.
 
+Unset Kernel Term Sharing.
+
+Axiom ispartlbinopabmonoidfracrel : forall ( X : abmonoid ) ( A : @subabmonoids X ) { L : hrel X } ( z : abmonoidfrac X A ) , @abmonoidfracrel X A ( ( admit + z ) )admit.
+
+Axiom ispartlbinopabmonoidfracrel' : $(let t:= eval unfold ispartlbinopabmonoidfracrel_type in
+                                      ispartlbinopabmonoidfracrel_type in exact t)$.
+
-- 
cgit v1.2.3