diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-20 13:04:45 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-20 14:05:54 +0200 |
| commit | cc42541eeaaec0371940e07efdb009a4ee74e468 (patch) | |
| tree | 6c8d5f3986551cd87027c3417a091b20a97f0f08 /tactics/contradiction.ml | |
| parent | f5d8d305c34f9bab21436c765aeeb56a65005dfe (diff) | |
Boxing the Goal.enter primitive into a record type.
Diffstat (limited to 'tactics/contradiction.ml')
| -rw-r--r-- | tactics/contradiction.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 7deb4baf6..34886d74d 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -48,13 +48,13 @@ let filter_hyp f tac = | [] -> Proofview.tclZERO Not_found | (id,_,t)::rest when f t -> tac id | _::rest -> seek rest in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in seek hyps - end + end } let contradiction_context = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let rec seek_neg l = match l with @@ -67,11 +67,11 @@ let contradiction_context = else match kind_of_term typ with | Prod (na,t,u) when is_empty_type u -> (Proofview.tclORELSE - (Proofview.Goal.enter begin fun gl -> + (Proofview.Goal.enter { enter = begin fun gl -> let is_conv_leq = Tacmach.New.pf_apply is_conv_leq gl in filter_hyp (fun typ -> is_conv_leq typ t) (fun id' -> simplest_elim (mkApp (mkVar id,[|mkVar id'|]))) - end) + end }) begin function (e, info) -> match e with | Not_found -> seek_neg rest | e -> Proofview.tclZERO ~info e @@ -80,7 +80,7 @@ let contradiction_context = in let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in seek_neg hyps - end + end } let is_negation_of env sigma typ t = match kind_of_term (whd_betadeltaiota env sigma t) with @@ -90,7 +90,7 @@ let is_negation_of env sigma typ t = | _ -> false let contradiction_term (c,lbind as cl) = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let type_of = Tacmach.New.pf_unsafe_type_of gl in @@ -113,7 +113,7 @@ let contradiction_term (c,lbind as cl) = | Not_found -> Tacticals.New.tclZEROMSG (Pp.str"Not a contradiction.") | e -> Proofview.tclZERO ~info e end - end + end } let contradiction = function | None -> Tacticals.New.tclTHEN intros contradiction_context |