Merge branch 'v8.6'

30 files changed, 159 insertions, 93 deletions

diff --git a/CHANGES b/CHANGES
index 594bbc831..c3eaae6ee 100644
--- a/CHANGES
+++ b/CHANGES
@@ -50,9 +50,10 @@ Tactics
 - Every generic argument type declares a tactic scope of the form "name:(...)"
   where name is the name of the argument. This generalizes the constr: and ltac:
   instances.
-- When in strict mode (i.e. in a Ltac definition) the "intro" tactic cannot use
-  a locally free identifier anymore. It must use e.g. the "fresh" primitive
-  instead (potential source of incompatibilities).
+- When in strict mode (i.e. in a Ltac definition), if the "intro" tactic is
+  given a free identifier, it is not bound in subsequent tactics anymore.
+  In order to introduce a binding, use e.g. the "fresh" primitive instead
+  (potential source of incompatibilities).
 - New tactics is_ind, is_const, is_proj, is_constructor for use in Ltac (DOC TODO).
 - New goal selectors.  Sets of goals can be selected by select by listing
   integers ranges. Example: "1,4-7,24: tac" focuses "tac" on goals 1,4,5,6,7,24.
@@ -61,6 +62,10 @@ Tactics
   "Structural Injection". In this case, hypotheses are also put in the
   context in the natural left-to-right order and the hypothesis on
   which injection applies is cleared.
+- Tactic "contradiction" (hence "easy") now also solve goals with
+  hypotheses of the form "~True" or "t<>t" (possible source of
+  incompatibilities because of more successes in automation, but
+  generally a more intuitive strategy).
 
 Hints
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 8172b5771..65b49893b 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1491,10 +1491,10 @@ the local context.
 \tacindex{contradiction}
 
 This tactic applies to any goal. The {\tt contradiction} tactic
-attempts to find in the current context (after all {\tt intros}) one
-hypothesis that is equivalent to {\tt False}. It permits to prune
-irrelevant cases. This tactic is a macro for the tactics sequence
-{\tt intros; elimtype False; assumption}.
+attempts to find in the current context (after all {\tt intros}) an
+hypothesis that is equivalent to an empty inductive type (e.g. {\tt
+  False}), to the negation of a singleton inductive type (e.g. {\tt
+  True} or {\tt x=x}), or two contradictory hypotheses.
 
 \begin{ErrMsgs}
 \item \errindex{No such assumption}
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index 10271ce0c..9962ce996 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -102,7 +102,7 @@ generator using for instance the command:
 
 This command generates a file \texttt{Makefile} that can be used to
 compile all the sources of the current project. It follows the
-syntax described by the output of \texttt{\% coq\_makefile ----help}.
+syntax described by the output of \texttt{\% coq\_makefile -{}-help}.
 Once the \texttt{Makefile} file has been generated a first time, it
 can be used by the \texttt{make} command to compile part or all of
 the project. Note that once it has been generated once, as soon as
@@ -112,8 +112,8 @@ automatically regenerated by an invocation of \texttt{make}.
 The following command generates a minimal example of
 \texttt{\_CoqProject} file:
 \begin{quotation}
-\texttt{\% \{ echo '-R .} \textit{MyFancyLib} \texttt{' ; find . -name
-  '*.v' -print \} > \_CoqProject}
+\texttt{\% ( echo "-R .\ }\textit{MyFancyLib}\texttt{" ; find .\ -name
+  "*.v" -print ) > \_CoqProject}
 \end{quotation}
 when executed at the root of the directory containing the
 project. Here the \texttt{\_CoqProject} lists all the \texttt{.v} files
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 51b3a7260..1ebc857d8 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1058,6 +1058,26 @@ module Goal = struct
     end
     end
 
+  exception NotExactlyOneSubgoal
+  let _ = CErrors.register_handler begin function
+  | NotExactlyOneSubgoal ->
+      CErrors.user_err (Pp.str"Not exactly one subgoal.")
+  | _ -> raise CErrors.Unhandled
+  end
+
+  let enter_one f =
+    let open Proof in
+    Comb.get >>= function
+    | [goal] -> begin
+       Env.get >>= fun env ->
+       tclEVARMAP >>= fun sigma ->
+       try f.enter (gmake env sigma goal)
+       with e when catchable_exception e ->
+         let (e, info) = CErrors.push e in
+         tclZERO ~info e
+      end
+    | _ -> tclZERO NotExactlyOneSubgoal
+
   type ('a, 'b) s_enter =
     { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma }
 
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 901cf26e0..bc68f11ff 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -499,6 +499,10 @@ module Goal : sig
   (** Like {!nf_enter}, but does not normalize the goal beforehand. *)
   val enter : ([ `LZ ], unit tactic) enter -> unit tactic
 
+  (** Like {!enter}, but assumes exactly one goal under focus, raising *)
+  (** an error otherwise. *)
+  val enter_one : ([ `LZ ], 'a tactic) enter -> 'a tactic
+
   type ('a, 'b) s_enter =
     { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma }
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 0e5602078..8520bd5d8 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -33,10 +33,10 @@ open Context.Rel.Declaration
 
 (** constr_expr -> glob_constr translation:
     - it adds holes for implicit arguments
-    - it remplaces notations by their value (scopes stuff are here)
+    - it replaces notations by their value (scopes stuff are here)
     - it recognizes global vars from local ones
-    - it prepares pattern maching problems (a pattern becomes a tree where nodes
-    are constructor/variable pairs and leafs are variables)
+    - it prepares pattern matching problems (a pattern becomes a tree
+      where nodes are constructor/variable pairs and leafs are variables)
 
     All that at once, fasten your seatbelt!
 *)
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 1e14eeb81..b020f8945 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -45,10 +45,10 @@ let dump_string s =
   if dump () && !glob_output != Feedback then 
     Pervasives.output_string !glob_file s
 
-let start_dump_glob vfile =
+let start_dump_glob ~vfile ~vofile =
   match !glob_output with
   | MultFiles ->
-      open_glob_file (Filename.chop_extension vfile ^ ".glob");
+      open_glob_file (Filename.chop_extension vofile ^ ".glob");
       output_string !glob_file "DIGEST ";
       output_string !glob_file (Digest.to_hex (Digest.file vfile));
       output_char !glob_file '\n'
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index a7c799114..e84a64052 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -9,7 +9,7 @@
 val open_glob_file : string -> unit
 val close_glob_file : unit -> unit
 
-val start_dump_glob : string -> unit
+val start_dump_glob : vfile:string -> vofile:string -> unit
 val end_dump_glob : unit -> unit
 
 val dump : unit -> bool
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 6b29b6d3d..2f3ebcc9b 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -125,7 +125,7 @@ let rec cases_pattern_fold_map loc g e = function
       e', PatCstr (loc,cstr,patl',na')
 
 let subst_binder_type_vars l = function
-  | Evar_kinds.BinderType (Name id) as e ->
+  | Evar_kinds.BinderType (Name id) ->
      let id =
        try match Id.List.assoc id l with GVar(_,id') -> id' | _ -> id
        with Not_found -> id in
diff --git a/library/lib.ml b/library/lib.ml
index 749cc4ff3..9401bc55b 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -501,13 +501,6 @@ let section_instance = function
 let is_in_section ref =
   try ignore (section_instance ref); true with Not_found -> false
 
-let full_replacement_context () = List.map pi2 !sectab
-let full_section_segment_of_constant con =
-  List.map (fun (vars,_,(x,_)) -> fun hyps ->
-    named_of_variable_context
-      (try pi1 (Names.Cmap.find con x)
-       with Not_found -> fst (extract_hyps (vars, hyps)))) !sectab
-
 (*************)
 (* Sections. *)
 
@@ -608,15 +601,6 @@ let rec dp_of_mp = function
   |Names.MPbound _ -> library_dp ()
   |Names.MPdot (mp,_) -> dp_of_mp mp
 
-let rec split_mp = function
-  |Names.MPfile dp -> dp, Names.DirPath.empty
-  |Names.MPdot (prfx, lbl) ->
-    let mprec, dprec = split_mp prfx in
-    mprec, Libnames.add_dirpath_suffix dprec (Names.Label.to_id lbl)
-  |Names.MPbound mbid ->
-    let (_,id,dp) = Names.MBId.repr mbid in
-    library_dp (), Names.DirPath.make [id]
-
 let rec split_modpath = function
   |Names.MPfile dp -> dp, []
   |Names.MPbound mbid -> library_dp (), [Names.MBId.to_id mbid]
@@ -628,20 +612,6 @@ let library_part = function
   |VarRef id -> library_dp ()
   |ref -> dp_of_mp (mp_of_global ref)
 
-let remove_section_part ref =
-  let sp = Nametab.path_of_global ref in
-  let dir,_ = repr_path sp in
-  match ref with
-  | VarRef id ->
-      anomaly (Pp.str "remove_section_part not supported on local variables")
-  | _ ->
-      if is_dirpath_prefix_of dir (cwd ()) then
-        (* Not yet (fully) discharged *)
-        pop_dirpath_n (sections_depth ()) (cwd ())
-      else
-	(* Theorem/Lemma outside its outer section of definition *)
-	dir
-
 (************************)
 (* Discharging names *)
 
diff --git a/library/lib.mli b/library/lib.mli
index 092643c2d..845727059 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -138,10 +138,8 @@ val library_dp : unit -> Names.DirPath.t
 
 (** Extract the library part of a name even if in a section *)
 val dp_of_mp : Names.module_path -> Names.DirPath.t
-val split_mp : Names.module_path -> Names.DirPath.t * Names.DirPath.t
 val split_modpath : Names.module_path -> Names.DirPath.t * Names.Id.t list
 val library_part :  Globnames.global_reference -> Names.DirPath.t
-val remove_section_part : Globnames.global_reference -> Names.DirPath.t
 
 (** {6 Sections } *)
 
@@ -190,10 +188,3 @@ val discharge_kn :  Names.mutual_inductive -> Names.mutual_inductive
 val discharge_con : Names.constant -> Names.constant
 val discharge_global : Globnames.global_reference -> Globnames.global_reference
 val discharge_inductive : Names.inductive -> Names.inductive
-
-(* discharging a constant in one go *)
-val full_replacement_context : unit -> Opaqueproof.work_list list
-val full_section_segment_of_constant :
-  Names.constant -> (Context.Named.t -> Context.Named.t) list
-
-
diff --git a/ltac/pptactic.ml b/ltac/pptactic.ml
index 5f2617e44..80cafb3ab 100644
--- a/ltac/pptactic.ml
+++ b/ltac/pptactic.ml
@@ -669,7 +669,7 @@ module Make
       let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in
       let pr_red_expr = pr_red_expr (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in
 
-      let pr_constrarg c = spc () ++ pr.pr_constr c in
+      let _pr_constrarg c = spc () ++ pr.pr_constr c in
       let pr_lconstrarg c = spc () ++ pr.pr_lconstr c in
       let pr_intarg n = spc () ++ int n in
 
@@ -717,7 +717,7 @@ module Make
                   prlist pr_binder_fix bll ++ annot ++ str" :" ++
                   pr_lconstrarg ty ++ str")") in
       (*  spc() ++
-          hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg
+          hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ _pr_constrarg
           c)
       *)
       let pr_cofix_tac (id,c) =
diff --git a/ltac/taccoerce.ml b/ltac/taccoerce.ml
index 2af872daf..df38a42cb 100644
--- a/ltac/taccoerce.ml
+++ b/ltac/taccoerce.ml
@@ -235,13 +235,15 @@ let coerce_to_closed_constr env v =
 let coerce_to_evaluable_ref env v =
   let fail () = raise (CannotCoerceTo "an evaluable reference") in
   let v = Value.normalize v in
+  let ev =
   if has_type v (topwit wit_intro_pattern) then
     match out_gen (topwit wit_intro_pattern) v with
     | _, IntroNaming (IntroIdentifier id) when is_variable env id -> EvalVarRef id
     | _ -> fail ()
   else if has_type v (topwit wit_var) then
-    let ev = EvalVarRef (out_gen (topwit wit_var) v) in
-    if Tacred.is_evaluable env ev then ev else fail ()
+    let id = out_gen (topwit wit_var) v in
+    if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id
+    else fail ()
   else if has_type v (topwit wit_ref) then
     let open Globnames in
     let r = out_gen (topwit wit_ref) v in
@@ -250,12 +252,11 @@ let coerce_to_evaluable_ref env v =
     | ConstRef c -> EvalConstRef c
     | IndRef _ | ConstructRef _ -> fail ()
   else
-    let ev = match Value.to_constr v with
+    match Value.to_constr v with
     | Some c when isConst c -> EvalConstRef (Univ.out_punivs (destConst c))
     | Some c when isVar c -> EvalVarRef (destVar c)
     | _ -> fail ()
-    in
-    if Tacred.is_evaluable env ev then ev else fail ()
+  in if Tacred.is_evaluable env ev then ev else fail ()
 
 let coerce_to_constr_list env v =
   let v = Value.to_list v in
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 9560bf2a3..07e4ddf84 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -449,7 +449,6 @@ let extend_constr state forpat ng =
     let isforpat = target_to_bool forpat in
     let needed_levels, state = register_empty_levels state isforpat pure_sublevels in
     let (pos,p4assoc,name,reinit), state = find_position state isforpat assoc level in
-    let nb_decls = List.length needed_levels + 1 in
     let empty_rules = List.map (prepare_empty_levels isforpat) needed_levels in
     let empty = { constrs = []; constrlists = []; binders = [] } in
     let act = ty_eval r (make_act forpat ng.notgram_notation) empty in
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index bedf925e8..c265103a6 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -904,7 +904,7 @@ let pr_ssrpattern_roundp  _ _ _ = pr_pattern_roundp
 let wit_rpatternty = add_genarg "rpatternty" pr_pattern
 
 let glob_ssrterm gs = function
-  | k, (_, Some c) as x -> k, 
+  | k, (_, Some c) -> k,
       let x = Tacintern.intern_constr gs c in
       fst x, Some c
   | ct -> ct
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 594732a5a..5653b5675 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1600,14 +1600,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
     let hyp = NamedDecl.get_id d in
     match occurrences_of_hyp hyp occs with
     | NoOccurrences, InHyp ->
-        if indirectly_dependent c d depdecls then
-          (* Told explicitly not to abstract over [d], but it is dependent *)
-          let id' = indirect_dependency d depdecls in
-          user_err  (str "Cannot abstract over " ++ Nameops.pr_id id'
-            ++ str " without also abstracting or erasing " ++ Nameops.pr_id hyp
-            ++ str ".")
-        else
-          (push_named_context_val d sign,depdecls)
+        (push_named_context_val d sign,depdecls)
     | AllOccurrences, InHyp as occ ->
         let occ = if likefirst then LikeFirst else AtOccs occ in
         let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 28952b9a7..ecc461f78 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -53,7 +53,8 @@ let typecheck_proof c concl env sigma =
 let (pr_constrv,pr_constr) =
   Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") ()
 
-let refine ?(unsafe = true) f = Proofview.Goal.enter { enter = begin fun gl ->
+let make_refine_enter ?(unsafe = true) f =
+  { enter = fun gl ->
   let gl = Proofview.Goal.assume gl in
   let sigma = Proofview.Goal.sigma gl in
   let sigma = Sigma.to_evar_map sigma in
@@ -64,7 +65,7 @@ let refine ?(unsafe = true) f = Proofview.Goal.enter { enter = begin fun gl ->
   let prev_future_goals = Evd.future_goals sigma in
   let prev_principal_goal = Evd.principal_future_goal sigma in
   (** Create the refinement term *)
-  let (c, sigma) = Sigma.run (Evd.reset_future_goals sigma) f in
+  let ((v,c), sigma) = Sigma.run (Evd.reset_future_goals sigma) f in
   let evs = Evd.future_goals sigma in
   let evkmain = Evd.principal_future_goal sigma in
   (** Check that the introduced evars are well-typed *)
@@ -94,10 +95,18 @@ let refine ?(unsafe = true) f = Proofview.Goal.enter { enter = begin fun gl ->
   let comb = CList.map_filter (Proofview.Unsafe.advance sigma) (CList.rev evs) in
   let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in
   let trace () = Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)) in
-  Proofview.Trace.name_tactic trace (Proofview.tclUNIT ()) >>= fun () ->
-  Proofview.Unsafe.tclEVARS sigma >>= fun () ->
-  Proofview.Unsafe.tclSETGOALS comb
-end }
+  Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v ->
+  Proofview.Unsafe.tclEVARS sigma <*>
+  Proofview.Unsafe.tclSETGOALS comb <*>
+  Proofview.tclUNIT v
+  }
+
+let refine_one ?(unsafe = true) f =
+  Proofview.Goal.enter_one (make_refine_enter ~unsafe f)
+
+let refine ?(unsafe = true) f =
+  let f = { run = fun sigma -> let Sigma (c,sigma,p) = f.run sigma in Sigma (((),c),sigma,p) } in
+  Proofview.Goal.enter (make_refine_enter ~unsafe f)
 
 (** Useful definitions *)
 
diff --git a/proofs/refine.mli b/proofs/refine.mli
index a9798b704..3d140f036 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -30,6 +30,9 @@ val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
     tactic failures. If [unsafe] is [false] (default is [true]) [t] is
     type-checked beforehand. *)
 
+val refine_one : ?unsafe:bool -> ('a * Constr.t) Sigma.run -> 'a tactic
+(** A generalization of [refine] which assumes exactly one goal under focus *)
+
 (** {7 Helper functions} *)
 
 val with_type : Environ.env -> Evd.evar_map ->
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index c81705c1a..6b29f574c 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -43,6 +43,8 @@ let absurd c = absurd c
 
 (* Contradiction *)
 
+let use_negated_unit_or_eq_type () = Flags.version_strictly_greater Flags.V8_5
+
 (** [f] does not assume its argument to be [nf_evar]-ed. *)
 let filter_hyp f tac =
   let rec seek = function
@@ -68,6 +70,21 @@ let contradiction_context =
 	    simplest_elim (mkVar id)
 	  else match kind_of_term typ with
 	  | Prod (na,t,u) when is_empty_type u ->
+             let is_unit_or_eq =
+               if use_negated_unit_or_eq_type () then match_with_unit_or_eq_type t
+               else None in
+	     Tacticals.New.tclORELSE
+               (match is_unit_or_eq with
+               | Some _ ->
+                   let hd,args = decompose_app t in
+                   let (ind,_ as indu) = destInd hd in
+                   let nparams = Inductiveops.inductive_nparams_env env ind in
+                   let params = Util.List.firstn nparams args in
+                   let p = applist ((mkConstructUi (indu,1)), params) in
+                   (* Checking on the fly that it type-checks *)
+                   simplest_elim (mkApp (mkVar id,[|p|]))
+               | None ->
+                 Tacticals.New.tclZEROMSG (Pp.str"Not a negated unit type."))
 	      (Proofview.tclORELSE
                  (Proofview.Goal.enter { enter = begin fun gl ->
                    let is_conv_leq = Tacmach.New.pf_apply is_conv_leq gl in
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 72c3523da..27af7200b 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -511,7 +511,7 @@ let coq_eqdec ~sum ~rev =
     let eqn = mkGAppRef coq_eq_ref (List.map mkGPatVar ["X1"; "X2"; "X3"]) in
     let args = [eqn; mkGAppRef coq_not_ref [eqn]] in
     let args = if rev then List.rev args else args in
-    mkPattern (mkGAppRef sum [eqn; mkGAppRef coq_not_ref [eqn]])
+    mkPattern (mkGAppRef sum args)
   )
 
 (** { ?X2 = ?X3 :> ?X1 } + { ~ ?X2 = ?X3 :> ?X1 } *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 9d0e9f084..49c91aa46 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1479,7 +1479,7 @@ let default_elim with_evars clear_flag (c,_ as cx) =
     begin function (e, info) -> match e with
       | IsNonrec ->
           (* For records, induction principles aren't there by default
-             anymore.  Instead, we do a case analysis instead. *)
+             anymore.  Instead, we do a case analysis. *)
           general_case_analysis with_evars clear_flag cx
       | e -> Proofview.tclZERO ~info e
     end
diff --git a/test-suite/bugs/closed/5078.v b/test-suite/bugs/closed/5078.v
new file mode 100644
index 000000000..ca73cbcc1
--- /dev/null
+++ b/test-suite/bugs/closed/5078.v
@@ -0,0 +1,5 @@
+(* Test coercion from ident to evaluable reference *)
+Tactic Notation "unfold_hyp" hyp(H) := cbv delta [H].
+Goal True -> Type.
+  intro H''.
+  Fail unfold_hyp H''.
diff --git a/test-suite/bugs/closed/5095.v b/test-suite/bugs/closed/5095.v
new file mode 100644
index 000000000..b6f38e3e8
--- /dev/null
+++ b/test-suite/bugs/closed/5095.v
@@ -0,0 +1,5 @@
+(* Checking let-in abstraction *)
+Goal let x := Set in let y := x in True.
+  intros x y.
+  (* There used to have a too strict dependency test there *)
+  set (s := Set) in (value of x).
diff --git a/test-suite/success/contradiction.v b/test-suite/success/contradiction.v
new file mode 100644
index 000000000..92a7c6ccb
--- /dev/null
+++ b/test-suite/success/contradiction.v
@@ -0,0 +1,32 @@
+(* Some tests for contradiction *)
+
+Lemma L1 : forall A B : Prop, A -> ~A -> B.
+Proof.
+intros; contradiction.
+Qed.
+
+Lemma L2 : forall A B : Prop, ~A -> A -> B.
+Proof.
+intros; contradiction.
+Qed.
+
+Lemma L3 : forall A : Prop, ~True -> A.
+Proof.
+intros; contradiction.
+Qed.
+
+Lemma L4 : forall A : Prop, forall x : nat, ~x=x -> A.
+Proof.
+intros; contradiction.
+Qed.
+
+Lemma L5 : forall A : Prop, forall x y : nat, ~x=y -> x=y -> A.
+Proof.
+intros; contradiction.
+Qed.
+
+Lemma L6 : forall A : Prop, forall x y : nat, x=y -> ~x=y -> A.
+Proof.
+intros; contradiction.
+Qed.
+
diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v
index 1f6af0dc4..724e2998e 100644
--- a/test-suite/success/eqdecide.v
+++ b/test-suite/success/eqdecide.v
@@ -14,6 +14,18 @@ Lemma lem1 : forall x y : T, {x = y} + {x <> y}.
  decide equality.
 Qed.
 
+Lemma lem1' : forall x y : T, x = y \/ x <> y.
+ decide equality.
+Qed.
+
+Lemma lem1'' : forall x y : T, {x <> y} + {x = y}.
+ decide equality.
+Qed.
+
+Lemma lem1''' : forall x y : T, x <> y \/ x = y.
+ decide equality.
+Qed.
+
 Lemma lem2 : forall x y : T, {x = y} + {x <> y}.
 intros x y.
  decide equality.
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 63fb5800c..fec6e0683 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -147,7 +147,7 @@ Module Make (NN:NType) <: ZType.
  Proof.
  apply Bool.eq_iff_eq_true.
  rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare.
- destruct Z.compare; split; try easy. now destruct 1.
+ now destruct Z.compare; split.
  Qed.
 
  Definition min n m := match compare n m with Gt => m | _ => n end.
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index 98949736c..1425041a1 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -338,7 +338,7 @@ Module Make (W0:CyclicType) <: NType.
  Proof.
  apply eq_iff_eq_true.
  rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare.
- destruct Z.compare; split; try easy. now destruct 1.
+ now destruct Z.compare; split.
  Qed.
 
  Definition min (n m : t) : t := match compare n m with Gt => m | _ => n end.
diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v
index 954d3df20..6f8fc1b32 100644
--- a/theories/Structures/OrdersFacts.v
+++ b/theories/Structures/OrdersFacts.v
@@ -448,7 +448,7 @@ Lemma leb_compare x y :
  (x <=? y) = match compare x y with Gt => false | _ => true end.
 Proof.
 apply eq_true_iff_eq. rewrite leb_le, <- compare_le_iff.
-destruct compare; split; try easy. now destruct 1.
+now destruct compare.
 Qed.
 
 End BoolOrderFacts.
diff --git a/toplevel/command.ml b/toplevel/command.ml
index caa20b534..ef918ef8d 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -142,21 +142,21 @@ let check_definition (ce, evd, _, imps) =
   check_evars_are_solved (Global.env ()) evd (Evd.empty,evd);
   ce
 
-let warn_local_let_definition =
-  CWarnings.create ~name:"local-let-definition" ~category:"scope"
-         (fun id ->
-          pr_id id ++ strbrk " is declared as a local definition")
+let warn_local_declaration =
+  CWarnings.create ~name:"local-declaration" ~category:"scope"
+         (fun (id,kind) ->
+          pr_id id ++ strbrk " is declared as a local " ++ str kind)
 
-let get_locality id = function
+let get_locality id ~kind = function
 | Discharge ->
   (** If a Let is defined outside a section, then we consider it as a local definition *)
-   warn_local_let_definition id;
+   warn_local_declaration (id,kind);
   true
 | Local -> true
 | Global -> false
 
 let declare_global_definition ident ce local k pl imps =
-  let local = get_locality ident local in
+  let local = get_locality ident ~kind:"definition" local in
   let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
   let gr = ConstRef kn in
   let () = maybe_declare_manual_implicits false gr imps in
@@ -240,7 +240,7 @@ match local with
   (r,Univ.Instance.empty,true)
 
 | Global | Local | Discharge ->
-  let local = get_locality ident local in
+  let local = get_locality ident ~kind:"axiom" local in
   let inl = match nl with
     | NoInline -> None
     | DefaultInline -> Some (Flags.get_inline_level())
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 3d573b365..07bccb532 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -345,7 +345,7 @@ let compile verbosely f =
       Aux_file.(start_aux_file
         ~aux_file:(aux_file_name_for long_f_dot_vo)
         ~v_file:long_f_dot_v);
-      Dumpglob.start_dump_glob long_f_dot_v;
+      Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo;
       Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
       if !Flags.xml_export then Hook.get f_xml_start_library ();
       let wall_clock1 = Unix.gettimeofday () in