diff options
| author | Pierre-Marie Pédrot | 2018-09-25 10:43:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-25 10:43:57 +0200 |
| commit | 7eb8a7eb8d23ffaf149f71a46fb1b089b90db7f8 (patch) | |
| tree | aa480ca16c64e5c1e04ac31dd9bc8066f44840c1 /plugins/omega | |
| parent | 4ae5a0e2dec60f753d21385b88991a9d1f0ec62d (diff) | |
| parent | 6b61b63bb8626827708024cbea1312a703a54124 (diff) | |
Merge PR #6343: [engine] Remove and deprecate `nf_enter` et al.
Diffstat (limited to 'plugins/omega')
| -rw-r--r-- | plugins/omega/coq_omega.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index e14c4e2ec1..abae6940fa 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -588,7 +588,7 @@ let abstract_path sigma typ path t = let focused_simpl path = let open Tacmach.New in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let newc = context (project gl) (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in convert_concl_no_check newc DEFAULTcast end @@ -656,7 +656,7 @@ let new_hole env sigma c = let clever_rewrite_base_poly typ p result theorem = let open Tacmach.New in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let full = pf_concl gl in let env = pf_env gl in let (abstracted,occ) = abstract_path (project gl) typ (List.rev p) full in @@ -708,7 +708,7 @@ let refine_app gl t = let clever_rewrite p vpath t = let open Tacmach.New in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let full = pf_concl gl in let (abstracted,occ) = abstract_path (project gl) (Lazy.force coq_Z) (List.rev p) full in let vargs = List.map (fun p -> occurrence (project gl) p occ) vpath in @@ -1763,7 +1763,7 @@ let onClearedName id tac = (* so renaming may be necessary *) tclTHEN (tclTRY (clear [id])) - (Proofview.Goal.nf_enter begin fun gl -> + (Proofview.Goal.enter begin fun gl -> let id = fresh_id Id.Set.empty id gl in tclTHEN (introduction id) (tac id) end) @@ -1771,7 +1771,7 @@ let onClearedName id tac = let onClearedName2 id tac = tclTHEN (tclTRY (clear [id])) - (Proofview.Goal.nf_enter begin fun gl -> + (Proofview.Goal.enter begin fun gl -> let id1 = fresh_id Id.Set.empty (add_suffix id "_left") gl in let id2 = fresh_id Id.Set.empty (add_suffix id "_right") gl in tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ] @@ -1956,7 +1956,7 @@ let destructure_goal = try let dec = decidability t in tclTHEN - (Proofview.Goal.nf_enter begin fun gl -> + (Proofview.Goal.enter begin fun gl -> refine_app gl (mkApp (Lazy.force coq_dec_not_not, [| t; dec |])) end) intro |