Merge branch 'v8.6'

3 files changed, 19 insertions, 2 deletions

diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index c81705c1a0..6b29f574cc 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 72c3523da0..27af7200bd 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 9d0e9f0842..49c91aa464 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