From 93a77f3cb8ee36072f93b4c0ace6f0f9c19f51a3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Mar 2016 18:41:37 +0100 Subject: Moving Refine to its proper module. --- dev/printers.mllib | 1 + printing/printer.ml | 2 +- proofs/proof.ml | 28 ++++++----- proofs/proofs.mllib | 1 + proofs/proofview.ml | 117 +-------------------------------------------- proofs/proofview.mli | 41 +++------------- proofs/refine.ml | 122 +++++++++++++++++++++++++++++++++++++++++++++++ proofs/refine.mli | 37 ++++++++++++++ tactics/extratactics.ml4 | 2 +- tactics/inv.ml | 2 +- tactics/rewrite.ml | 6 +-- tactics/tactics.ml | 32 ++++++------- tactics/tactics.mli | 2 +- toplevel/classes.ml | 2 +- 14 files changed, 209 insertions(+), 186 deletions(-) create mode 100644 proofs/refine.ml create mode 100644 proofs/refine.mli diff --git a/dev/printers.mllib b/dev/printers.mllib index 7710033db..c46f6b72a 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -184,6 +184,7 @@ Proof_errors Logic_monad Proofview_monad Proofview +Refine Proof Proof_global Pfedit diff --git a/printing/printer.ml b/printing/printer.ml index b89005887..2e67fa5ff 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -50,7 +50,7 @@ let pr_lconstr_core goal_concl_style env sigma t = let pr_lconstr_env env = pr_lconstr_core false env let pr_constr_env env = pr_constr_core false env -let _ = Hook.set Proofview.Refine.pr_constr pr_constr_env +let _ = Hook.set Refine.pr_constr pr_constr_env let pr_lconstr_goal_style_env env = pr_lconstr_core true env let pr_constr_goal_style_env env = pr_constr_core true env diff --git a/proofs/proof.ml b/proofs/proof.ml index b604fde4e..86af420dc 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -334,22 +334,24 @@ let compact p = (*** Tactics ***) let run_tactic env tac pr = + let open Proofview.Notations in let sp = pr.proofview in - let (_,tacticced_proofview,(status,to_shelve,give_up),info_trace) = - Proofview.apply env tac sp + let undef sigma l = List.filter (fun g -> Evd.is_undefined sigma g) l in + let tac = + tac >>= fun () -> + Proofview.tclEVARMAP >>= fun sigma -> + (* Already solved goals are not to be counted as shelved. Nor are + they to be marked as unresolvable. *) + let retrieved = undef sigma (List.rev (Evd.future_goals sigma)) in + let sigma = List.fold_left Proofview.Unsafe.mark_as_goal sigma retrieved in + Proofview.Unsafe.tclEVARS sigma >>= fun () -> + Proofview.tclUNIT retrieved in - let sigma = Proofview.return tacticced_proofview in - (* Already solved goals are not to be counted as shelved. Nor are - they to be marked as unresolvable. *) - let undef l = List.filter (fun g -> Evd.is_undefined sigma g) l in - let retrieved = undef (List.rev (Evd.future_goals sigma)) in - let shelf = (undef pr.shelf)@retrieved@(undef to_shelve) in - let proofview = - List.fold_left - Proofview.Unsafe.mark_as_goal - tacticced_proofview - retrieved + let (retrieved,proofview,(status,to_shelve,give_up),info_trace) = + Proofview.apply env tac sp in + let sigma = Proofview.return proofview in + let shelf = (undef sigma pr.shelf)@retrieved@(undef sigma to_shelve) in let given_up = pr.given_up@give_up in let proofview = Proofview.Unsafe.reset_future_goals proofview in { pr with proofview ; shelf ; given_up },(status,info_trace) diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 08556d62e..236d47932 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -5,6 +5,7 @@ Proof_using Proof_errors Logic Proofview +Refine Proof Proof_global Redexpr diff --git a/proofs/proofview.ml b/proofs/proofview.ml index f42a60d9d..20be02e76 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -901,7 +901,7 @@ module Unsafe = struct let reset_future_goals p = { p with solution = Evd.reset_future_goals p.solution } - let mark_as_goal_evm evd content = + let mark_as_goal evd content = let info = Evd.find evd content in let info = { info with Evd.evar_source = match info.Evd.evar_source with @@ -911,8 +911,7 @@ module Unsafe = struct let info = Typeclasses.mark_unresolvable info in Evd.add evd content info - let mark_as_goal p gl = - { p with solution = mark_as_goal_evm p.solution gl } + let advance = advance end @@ -1075,118 +1074,6 @@ end -(** {6 The refine tactic} *) - -module Refine = -struct - - let extract_prefix env info = - let ctx1 = List.rev (Environ.named_context env) in - let ctx2 = List.rev (Evd.evar_context info) in - let rec share l1 l2 accu = match l1, l2 with - | d1 :: l1, d2 :: l2 -> - if d1 == d2 then share l1 l2 (d1 :: accu) - else (accu, d2 :: l2) - | _ -> (accu, l2) - in - share ctx1 ctx2 [] - - let typecheck_evar ev env sigma = - let info = Evd.find sigma ev in - (** Typecheck the hypotheses. *) - let type_hyp (sigma, env) decl = - let t = get_type decl in - let evdref = ref sigma in - let _ = Typing.e_sort_of env evdref t in - let () = match decl with - | LocalAssum _ -> () - | LocalDef (_,body,_) -> Typing.e_check env evdref body t - in - (!evdref, Environ.push_named decl env) - in - let (common, changed) = extract_prefix env info in - let env = Environ.reset_with_named_context (Environ.val_of_named_context common) env in - let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in - (** Typecheck the conclusion *) - let evdref = ref sigma in - let _ = Typing.e_sort_of env evdref (Evd.evar_concl info) in - !evdref - - let typecheck_proof c concl env sigma = - let evdref = ref sigma in - let () = Typing.e_check env evdref c concl in - !evdref - - let (pr_constrv,pr_constr) = - Hook.make ~default:(fun _env _sigma _c -> Pp.str"") () - - let refine ?(unsafe = true) f = Goal.enter { Goal.enter = begin fun gl -> - let sigma = Goal.sigma gl in - let sigma = Sigma.to_evar_map sigma in - let env = Goal.env gl in - let concl = Goal.concl gl in - (** Save the [future_goals] state to restore them after the - refinement. *) - let prev_future_goals = Evd.future_goals sigma in - let prev_principal_goal = Evd.principal_future_goal sigma in - (** Create the refinement term *) - let (c, sigma) = Sigma.run (Evd.reset_future_goals sigma) f in - let evs = Evd.future_goals sigma in - let evkmain = Evd.principal_future_goal sigma in - (** Check that the introduced evars are well-typed *) - let fold accu ev = typecheck_evar ev env accu in - let sigma = if unsafe then sigma else CList.fold_left fold sigma evs in - (** Check that the refined term is typesafe *) - let sigma = if unsafe then sigma else typecheck_proof c concl env sigma in - (** Check that the goal itself does not appear in the refined term *) - let _ = - if not (Evarutil.occur_evar_upto sigma gl.Goal.self c) then () - else Pretype_errors.error_occur_check env sigma gl.Goal.self c - in - (** Proceed to the refinement *) - let sigma = match evkmain with - | None -> Evd.define gl.Goal.self c sigma - | Some evk -> - let id = Evd.evar_ident gl.Goal.self sigma in - let sigma = Evd.define gl.Goal.self c sigma in - match id with - | None -> sigma - | Some id -> Evd.rename evk id sigma - in - (** Restore the [future goals] state. *) - let sigma = Evd.restore_future_goals sigma prev_future_goals prev_principal_goal in - (** Select the goals *) - let comb = undefined sigma (CList.rev evs) in - let sigma = CList.fold_left Unsafe.mark_as_goal_evm sigma comb in - let open Proof in - InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"refine"++spc()++ Hook.get pr_constrv env sigma c)))) >> - Pv.modify (fun ps -> { ps with solution = sigma; comb; }) - end } - - (** Useful definitions *) - - let with_type env evd c t = - let my_type = Retyping.get_type_of env evd c in - let j = Environ.make_judge c my_type in - let (evd,j') = - Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t - in - evd , j'.Environ.uj_val - - let refine_casted ?unsafe f = Goal.enter { Goal.enter = begin fun gl -> - let concl = Goal.concl gl in - let env = Goal.env gl in - let f = { run = fun h -> - let Sigma (c, h, p) = f.run h in - let sigma, c = with_type env (Sigma.to_evar_map h) c concl in - Sigma (c, Sigma.Unsafe.of_evar_map sigma, p) - } in - refine ?unsafe f - end } -end - - - (** {6 Trace} *) module Trace = struct diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 20f67f258..6bc2e9a0e 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -406,7 +406,13 @@ module Unsafe : sig (** Give an evar the status of a goal (changes its source location and makes it unresolvable for type classes. *) - val mark_as_goal : proofview -> Evar.t -> proofview + val mark_as_goal : Evd.evar_map -> Evar.t -> Evd.evar_map + + (** [advance sigma g] returns [Some g'] if [g'] is undefined and is + the current avatar of [g] (for instance [g] was changed by [clear] + into [g']). It returns [None] if [g] has been (partially) + solved. *) + val advance : Evd.evar_map -> Evar.t -> Evar.t option end (** This module gives access to the innards of the monad. Its use is @@ -491,39 +497,6 @@ module Goal : sig end -(** {6 The refine tactic} *) - -module Refine : sig - - (** Printer used to print the constr which refine refines. *) - val pr_constr : - (Environ.env -> Evd.evar_map -> Term.constr -> Pp.std_ppcmds) Hook.t - - (** {7 Refinement primitives} *) - - val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic - (** In [refine ?unsafe t], [t] is a term with holes under some - [evar_map] context. The term [t] is used as a partial solution - for the current goal (refine is a goal-dependent tactic), the - new holes created by [t] become the new subgoals. Exceptions - raised during the interpretation of [t] are caught and result in - tactic failures. If [unsafe] is [false] (default is [true]) [t] is - type-checked beforehand. *) - - (** {7 Helper functions} *) - - val with_type : Environ.env -> Evd.evar_map -> - Term.constr -> Term.types -> Evd.evar_map * Term.constr - (** [with_type env sigma c t] ensures that [c] is of type [t] - inserting a coercion if needed. *) - - val refine_casted : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic - (** Like {!refine} except the refined term is coerced to the conclusion of the - current goal. *) - -end - - (** {6 Trace} *) module Trace : sig diff --git a/proofs/refine.ml b/proofs/refine.ml new file mode 100644 index 000000000..db0b26f7e --- /dev/null +++ b/proofs/refine.ml @@ -0,0 +1,122 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + if d1 == d2 then share l1 l2 (d1 :: accu) + else (accu, d2 :: l2) + | _ -> (accu, l2) + in + share ctx1 ctx2 [] + +let typecheck_evar ev env sigma = + let info = Evd.find sigma ev in + (** Typecheck the hypotheses. *) + let type_hyp (sigma, env) decl = + let t = get_type decl in + let evdref = ref sigma in + let _ = Typing.e_sort_of env evdref t in + let () = match decl with + | LocalAssum _ -> () + | LocalDef (_,body,_) -> Typing.e_check env evdref body t + in + (!evdref, Environ.push_named decl env) + in + let (common, changed) = extract_prefix env info in + let env = Environ.reset_with_named_context (Environ.val_of_named_context common) env in + let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in + (** Typecheck the conclusion *) + let evdref = ref sigma in + let _ = Typing.e_sort_of env evdref (Evd.evar_concl info) in + !evdref + +let typecheck_proof c concl env sigma = + let evdref = ref sigma in + let () = Typing.e_check env evdref c concl in + !evdref + +let (pr_constrv,pr_constr) = + Hook.make ~default:(fun _env _sigma _c -> Pp.str"") () + +let refine ?(unsafe = true) f = Proofview.Goal.enter { enter = begin fun gl -> + let gl = Proofview.Goal.assume gl in + let sigma = Proofview.Goal.sigma gl in + let sigma = Sigma.to_evar_map sigma in + let env = Proofview.Goal.env gl in + let concl = Proofview.Goal.concl gl in + (** Save the [future_goals] state to restore them after the + refinement. *) + let prev_future_goals = Evd.future_goals sigma in + let prev_principal_goal = Evd.principal_future_goal sigma in + (** Create the refinement term *) + let (c, sigma) = Sigma.run (Evd.reset_future_goals sigma) f in + let evs = Evd.future_goals sigma in + let evkmain = Evd.principal_future_goal sigma in + (** Check that the introduced evars are well-typed *) + let fold accu ev = typecheck_evar ev env accu in + let sigma = if unsafe then sigma else CList.fold_left fold sigma evs in + (** Check that the refined term is typesafe *) + let sigma = if unsafe then sigma else typecheck_proof c concl env sigma in + (** Check that the goal itself does not appear in the refined term *) + let self = Proofview.Goal.goal gl in + let _ = + if not (Evarutil.occur_evar_upto sigma self c) then () + else Pretype_errors.error_occur_check env sigma self c + in + (** Proceed to the refinement *) + let sigma = match evkmain with + | None -> Evd.define self c sigma + | Some evk -> + let id = Evd.evar_ident self sigma in + let sigma = Evd.define self c sigma in + match id with + | None -> sigma + | Some id -> Evd.rename evk id sigma + in + (** Restore the [future goals] state. *) + let sigma = Evd.restore_future_goals sigma prev_future_goals prev_principal_goal in + (** Select the goals *) + let comb = CList.map_filter (Proofview.Unsafe.advance sigma) (CList.rev evs) in + let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in + let trace () = Pp.(hov 2 (str"refine"++spc()++ Hook.get pr_constrv env sigma c)) in + Proofview.Trace.name_tactic trace (Proofview.tclUNIT ()) >>= fun () -> + Proofview.Unsafe.tclEVARS sigma >>= fun () -> + Proofview.Unsafe.tclSETGOALS comb +end } + +(** Useful definitions *) + +let with_type env evd c t = + let my_type = Retyping.get_type_of env evd c in + let j = Environ.make_judge c my_type in + let (evd,j') = + Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t + in + evd , j'.Environ.uj_val + +let refine_casted ?unsafe f = Proofview.Goal.enter { enter = begin fun gl -> + let gl = Proofview.Goal.assume gl in + let concl = Proofview.Goal.concl gl in + let env = Proofview.Goal.env gl in + let f = { run = fun h -> + let Sigma (c, h, p) = f.run h in + let sigma, c = with_type env (Sigma.to_evar_map h) c concl in + Sigma (c, Sigma.Unsafe.of_evar_map sigma, p) + } in + refine ?unsafe f +end } diff --git a/proofs/refine.mli b/proofs/refine.mli new file mode 100644 index 000000000..17c7e28ca --- /dev/null +++ b/proofs/refine.mli @@ -0,0 +1,37 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Evd.evar_map -> Term.constr -> Pp.std_ppcmds) Hook.t + +(** {7 Refinement primitives} *) + +val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic +(** In [refine ?unsafe t], [t] is a term with holes under some + [evar_map] context. The term [t] is used as a partial solution + for the current goal (refine is a goal-dependent tactic), the + new holes created by [t] become the new subgoals. Exceptions + raised during the interpretation of [t] are caught and result in + tactic failures. If [unsafe] is [false] (default is [true]) [t] is + type-checked beforehand. *) + +(** {7 Helper functions} *) + +val with_type : Environ.env -> Evd.evar_map -> + Term.constr -> Term.types -> Evd.evar_map * Term.constr +(** [with_type env sigma c t] ensures that [c] is of type [t] + inserting a coercion if needed. *) + +val refine_casted : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic +(** Like {!refine} except the refined term is coerced to the conclusion of the + current goal. *) diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 0cc796886..23aa8dcb4 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -370,7 +370,7 @@ let refine_tac ist simple c = let expected_type = Pretyping.OfType concl in let c = Tacinterp.type_uconstr ~flags ~expected_type ist c in let update = { run = fun sigma -> c.delayed env sigma } in - let refine = Proofview.Refine.refine ~unsafe:false update in + let refine = Refine.refine ~unsafe:false update in if simple then refine else refine <*> Tactics.New.reduce_after_refine <*> diff --git a/tactics/inv.ml b/tactics/inv.ml index 6841ab0ec..89c6beb32 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -459,7 +459,7 @@ let raw_inversion inv_kind id status names = in let refined id = let prf = mkApp (mkVar id, args) in - Proofview.Refine.refine { run = fun h -> Sigma (prf, h, Sigma.refl) } + Refine.refine { run = fun h -> Sigma (prf, h, Sigma.refl) } in let neqns = List.length realargs in let as_mode = names != None in diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 67d21886b..4c06550d4 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1539,7 +1539,7 @@ let assert_replacing id newt tac = | d :: rem -> insert_dependent env (LocalAssum (get_id d, newt)) [] after @ rem in let env' = Environ.reset_with_named_context (val_of_named_context nc) env in - Proofview.Refine.refine ~unsafe:false { run = begin fun sigma -> + Refine.refine ~unsafe:false { run = begin fun sigma -> let Sigma (ev, sigma, p) = Evarutil.new_evar env' sigma concl in let Sigma (ev', sigma, q) = Evarutil.new_evar env sigma newt in let map d = @@ -1568,7 +1568,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let gls = List.rev (Evd.fold_undefined fold undef []) in match clause, prf with | Some id, Some p -> - let tac = Proofview.Refine.refine ~unsafe:false { run = fun h -> Sigma (p, h, Sigma.refl) } <*> Proofview.Unsafe.tclNEWGOALS gls in + let tac = Refine.refine ~unsafe:false { run = fun h -> Sigma (p, h, Sigma.refl) } <*> Proofview.Unsafe.tclNEWGOALS gls in Proofview.Unsafe.tclEVARS undef <*> assert_replacing id newt tac | Some id, None -> @@ -1582,7 +1582,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let Sigma (ev, sigma, q) = Evarutil.new_evar env sigma newt in Sigma (mkApp (p, [| ev |]), sigma, q) end } in - Proofview.Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls + Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls end } | None, None -> Proofview.Unsafe.tclEVARS undef <*> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ffe10d81c..7ae178af5 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -163,7 +163,7 @@ let _ = does not check anything. *) let unsafe_intro env store decl b = let open Context.Named.Declaration in - Proofview.Refine.refine ~unsafe:true { run = begin fun sigma -> + Refine.refine ~unsafe:true { run = begin fun sigma -> let ctx = named_context_val env in let nctx = push_named_context_val decl ctx in let inst = List.map (mkVar % get_id) (named_context env) in @@ -199,7 +199,7 @@ let convert_concl ?(check=true) ty k = let env = Proofview.Goal.env gl in let store = Proofview.Goal.extra gl in let conclty = Proofview.Goal.raw_concl gl in - Proofview.Refine.refine ~unsafe:true { run = begin fun sigma -> + Refine.refine ~unsafe:true { run = begin fun sigma -> let Sigma ((), sigma, p) = if check then begin let sigma = Sigma.to_evar_map sigma in @@ -222,7 +222,7 @@ let convert_hyp ?(check=true) d = let store = Proofview.Goal.extra gl in let sign = convert_hyp check (named_context_val env) sigma d in let env = reset_with_named_context sign env in - Proofview.Refine.refine ~unsafe:true { run = begin fun sigma -> + Refine.refine ~unsafe:true { run = begin fun sigma -> Evarutil.new_evar env sigma ~principal:true ~store ty end } end } @@ -345,7 +345,7 @@ let rename_hyp repl = let nconcl = subst concl in let nctx = Environ.val_of_named_context nhyps in let instance = List.map (mkVar % get_id) hyps in - Proofview.Refine.refine ~unsafe:true { run = begin fun sigma -> + Refine.refine ~unsafe:true { run = begin fun sigma -> Evarutil.new_evar_instance nctx sigma nconcl ~store instance end } end } @@ -1070,7 +1070,7 @@ let cut c = let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_of_hyps gl) in (** Backward compat: normalize [c]. *) let c = if normalize_cut then local_strong whd_betaiota sigma c else c in - Proofview.Refine.refine ~unsafe:true { run = begin fun h -> + Refine.refine ~unsafe:true { run = begin fun h -> let Sigma (f, h, p) = Evarutil.new_evar ~principal:true env h (mkArrow c (Vars.lift 1 concl)) in let Sigma (x, h, q) = Evarutil.new_evar env h c in let f = mkLetIn (Name id, x, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in @@ -1736,7 +1736,7 @@ let cut_and_apply c = | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) -> let concl = Proofview.Goal.concl gl in let env = Tacmach.New.pf_env gl in - Proofview.Refine.refine { run = begin fun sigma -> + Refine.refine { run = begin fun sigma -> let typ = mkProd (Anonymous, c2, concl) in let Sigma (f, sigma, p) = Evarutil.new_evar env sigma typ in let Sigma (x, sigma, q) = Evarutil.new_evar env sigma c1 in @@ -1757,7 +1757,7 @@ let cut_and_apply c = (* let refine_no_check = Profile.profile2 refine_no_checkkey refine_no_check *) let new_exact_no_check c = - Proofview.Refine.refine ~unsafe:true { run = fun h -> Sigma.here c h } + Refine.refine ~unsafe:true { run = fun h -> Sigma.here c h } let exact_check c = Proofview.Goal.s_enter { s_enter = begin fun gl -> @@ -1808,7 +1808,7 @@ let assumption = in if is_same_type then (Proofview.Unsafe.tclEVARS sigma) <*> - Proofview.Refine.refine ~unsafe:true { run = fun h -> Sigma.here (mkVar (get_id decl)) h } + Refine.refine ~unsafe:true { run = fun h -> Sigma.here (mkVar (get_id decl)) h } else arec gl only_eq rest in let assumption_tac = { enter = begin fun gl -> @@ -1893,7 +1893,7 @@ let clear_body ids = check_is_type env concl msg in check_hyps <*> check_concl <*> - Proofview.Refine.refine ~unsafe:true { run = begin fun sigma -> + Refine.refine ~unsafe:true { run = begin fun sigma -> Evarutil.new_evar env sigma ~principal:true concl end } end } @@ -1950,7 +1950,7 @@ let apply_type newcl args = Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let store = Proofview.Goal.extra gl in - Proofview.Refine.refine { run = begin fun sigma -> + Refine.refine { run = begin fun sigma -> let newcl = nf_betaiota (Sigma.to_evar_map sigma) newcl (* As in former Logic.refine *) in let Sigma (ev, sigma, p) = Evarutil.new_evar env sigma ~principal:true ~store newcl in @@ -1971,7 +1971,7 @@ let bring_hyps hyps = let concl = Tacmach.New.pf_nf_concl gl in let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in let args = Array.of_list (Context.Named.to_instance hyps) in - Proofview.Refine.refine { run = begin fun sigma -> + Refine.refine { run = begin fun sigma -> let Sigma (ev, sigma, p) = Evarutil.new_evar env sigma ~principal:true ~store newcl in Sigma (mkApp (ev, args), sigma, p) @@ -2671,7 +2671,7 @@ let new_generalize_gen_let lconstr = 0 lconstr (concl, sigma, []) in let tac = - Proofview.Refine.refine { run = begin fun sigma -> + Refine.refine { run = begin fun sigma -> let Sigma (ev, sigma, p) = Evarutil.new_evar env sigma ~principal:true newcl in Sigma ((applist (ev, args)), sigma, p) end } @@ -3325,7 +3325,7 @@ let mk_term_eq env sigma ty t ty' t' = let make_abstract_generalize env id typ concl dep ctx body c eqs args refls = let open Context.Rel.Declaration in - Proofview.Refine.refine { run = begin fun sigma -> + Refine.refine { run = begin fun sigma -> let eqslen = List.length eqs in (* Abstract by the "generalized" hypothesis equality proof if necessary. *) let abshypeq, abshypt = @@ -4126,7 +4126,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim (* and destruct has side conditions first *) Tacticals.New.tclTHENLAST) (Tacticals.New.tclTHENLIST [ - Proofview.Refine.refine ~unsafe:true { run = begin fun sigma -> + Refine.refine ~unsafe:true { run = begin fun sigma -> let b = not with_evars && with_eq != None in let Sigma (c, sigma, p) = use_bindings env sigma elim b (c0,lbind) t0 in let t = Retyping.get_type_of env (Sigma.to_evar_map sigma) c in @@ -4150,7 +4150,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim let env = reset_with_named_context sign env in let tac = Tacticals.New.tclTHENLIST [ - Proofview.Refine.refine ~unsafe:true { run = begin fun sigma -> + Refine.refine ~unsafe:true { run = begin fun sigma -> mkletin_goal env sigma store with_eq true (id,lastlhyp,ccl,c) None end }; tac @@ -4795,6 +4795,6 @@ module New = struct {onhyps=None; concl_occs=AllOccurrences } let refine ?unsafe c = - Proofview.Refine.refine ?unsafe c <*> + Refine.refine ?unsafe c <*> reduce_after_refine end diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 26ea01769..4c4a96ec0 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -431,7 +431,7 @@ end module New : sig val refine : ?unsafe:bool -> constr Sigma.run -> unit Proofview.tactic - (** [refine ?unsafe c] is [Proofview.Refine.refine ?unsafe c] + (** [refine ?unsafe c] is [Refine.refine ?unsafe c] followed by beta-iota-reduction of the conclusion. *) val reduce_after_refine : unit Proofview.tactic diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 0a83c49c8..4bf0450d2 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -330,7 +330,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro if not (Option.is_empty term) then let init_refine = Tacticals.New.tclTHENLIST [ - Proofview.Refine.refine { run = fun evm -> Sigma (Option.get term, evm, Sigma.refl) }; + Refine.refine { run = fun evm -> Sigma (Option.get term, evm, Sigma.refl) }; Proofview.Unsafe.tclNEWGOALS gls; Tactics.New.reduce_after_refine; ] -- cgit v1.2.3