From 745c5325d79e754faecd0e1db75744f436f61a3b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 1 Sep 2016 21:59:17 +0200
Subject: Typo.

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

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f47141efbc..8dfb526325 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1475,7 +1475,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
-- 
cgit v1.2.3


From 6eede071cb97e1e39772c2bdecb5189c4fa2adb0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 21 Jan 2016 23:28:40 +0100
Subject: Extending "contradiction" so that it recognizes statements such as
 "~x=x" or ~True.

Found 1 incompatibility in tested contribs and 3 times the same
pattern of incompatibility in the standard library. In all cases, it
is an improvement in the form of the script.

New behavior deactivated when version is <= 8.5.
---
 tactics/contradiction.ml | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'tactics')

diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index c3796b4842..445a104d60 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -42,6 +42,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
@@ -67,6 +69,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
-- 
cgit v1.2.3


From e6eef565639fb3840dd235eb675ece6e4dbeb082 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 16 Sep 2016 15:46:31 +0200
Subject: Addressing OCaml compilation warnings.

One of them revealed a true bug.
---
 tactics/hipattern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 6e24cc4698..7b52a9cee6 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -509,7 +509,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 } *)
-- 
cgit v1.2.3