diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-23 18:56:18 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-23 18:56:18 +0200 |
commit | a52d06ea16cff00faa7d2f63ad5c1ca0b58e64b4 (patch) | |
tree | 40440d7daed82bd24180b36ef224f245ddca42f5 /tactics/contradiction.ml | |
parent | 30a908becf31d91592a1f7934cfa3df2d67d1834 (diff) | |
parent | a321074cdd2f9375662c7c9f17be5c045328bd82 (diff) |
Merge branch 'v8.6'
Diffstat (limited to 'tactics/contradiction.ml')
-rw-r--r-- | tactics/contradiction.ml | 17 |
1 files changed, 17 insertions, 0 deletions
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 |