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/contradiction.ml') diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index c3796b484..445a104d6 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