From 7267e31fa4456aee62a1e39dfdb7e38a8832f93f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 14 Feb 2018 09:07:46 +0100 Subject: ssr: ipats: V82.tactic ~nf_evars:false everywhere --- plugins/ssr/ssrbwd.ml | 14 +++++++------- plugins/ssr/ssrelim.ml | 9 ++++++--- plugins/ssr/ssrelim.mli | 5 ++++- plugins/ssr/ssripats.ml | 36 ++++++++++++++++++------------------ 4 files changed, 35 insertions(+), 29 deletions(-) (limited to 'plugins/ssr') diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml index daad730ff..23da1eb69 100644 --- a/plugins/ssr/ssrbwd.ml +++ b/plugins/ssr/ssrbwd.ml @@ -121,13 +121,13 @@ let refine_interp_apply_view dbl ist gl gv = else []) let apply_top_tac = - Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (introid top_id); - Proofview.V82.tactic (apply_rconstr (mkRVar top_id)); - Tactics.clear [top_id] + Tacticals.tclTHENLIST [ + introid top_id; + apply_rconstr (mkRVar top_id); + old_cleartac [SsrHyp(None,top_id)] ] -let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic (fun gl -> +let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic ~nf_evars:false (fun gl -> let _, clr = interp_hyps ist gl gclr in let vtac gv i gl' = refine_interp_apply_view i ist gl' gv in let ggenl, tclGENTAC = @@ -152,7 +152,7 @@ let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic (fun gl -> let gl = pf_merge_uc_of sigma gl in Tacticals.tclTHENLIST [old_cleartac clr; refine_with ~beta:true lemma; old_cleartac clr'] gl | _, _ -> - let open Proofview.Notations in - Proofview.V82.of_tactic (apply_top_tac <*> cleartac clr) gl) gl + Tacticals.tclTHENLIST [apply_top_tac; old_cleartac clr] gl) gl ) +let apply_top_tac = Proofview.V82.tactic ~nf_evars:false apply_top_tac diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index b3e59f7fc..a5d44d925 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -377,7 +377,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac let no_intro ?ist what eqid elim_tac is_rec clr = elim_tac let elimtac x = - Proofview.V82.tactic + Proofview.V82.tactic ~nf_evars:false (ssrelim ~is_case:false [] (`EConstr ([],None,x)) None no_intro) let casetac x = ssrelim ~is_case:true [] (`EConstr ([],None,x)) None no_intro @@ -435,6 +435,9 @@ let perform_injection c gl = let injtac = Tacticals.tclTHEN (introid id) (injectidl2rtac id id_with_ebind) in Tacticals.tclTHENLAST (Proofview.V82.of_tactic (Tactics.apply (EConstr.compose_lam dc cl1))) injtac gl -let ssrscasetac force_inj c = Proofview.V82.tactic (fun gl -> - if force_inj || is_injection_case c gl then perform_injection c gl +let ssrscase_or_inj_tac c = Proofview.V82.tactic ~nf_evars:false (fun gl -> + if is_injection_case c gl then perform_injection c gl else casetac c gl) + +let ssrscasetac c = + Proofview.V82.tactic ~nf_evars:false (fun gl -> casetac c gl) diff --git a/plugins/ssr/ssrelim.mli b/plugins/ssr/ssrelim.mli index b802486a0..0541a13ed 100644 --- a/plugins/ssr/ssrelim.mli +++ b/plugins/ssr/ssrelim.mli @@ -45,6 +45,9 @@ val perform_injection : Goal.goal Evd.sigma -> Goal.goal list Evd.sigma val ssrscasetac : - bool -> + EConstr.constr -> + unit Proofview.tactic + +val ssrscase_or_inj_tac : EConstr.constr -> unit Proofview.tactic diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 77ebe17a4..1a964bd50 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -137,9 +137,9 @@ let tac_case t = Ssrcommon.tacTYPEOF t >>= fun ty -> Ssrcommon.tacIS_INJECTION_CASE ~ty t >>= fun is_inj -> if is_inj then - V82.tactic (Ssrelim.perform_injection t) + V82.tactic ~nf_evars:false (Ssrelim.perform_injection t) else - Ssrelim.ssrscasetac false t + Ssrelim.ssrscasetac t end (** [=> [: id]] ************************************************************) @@ -218,7 +218,7 @@ let rec ipat_tac1 future_ipats ipat : unit tactic = tclIORPAT (Ssrcommon.tclWITHTOP tac_case) ipatss | IPatInj ipatss -> tclIORPAT (Ssrcommon.tclWITHTOP - (fun t -> V82.tactic (Ssrelim.perform_injection t))) ipatss + (fun t -> V82.tactic ~nf_evars:false (Ssrelim.perform_injection t))) ipatss | IPatAnon Drop -> intro_drop | IPatAnon One -> Ssrcommon.tclINTRO_ANON @@ -230,15 +230,15 @@ let rec ipat_tac1 future_ipats ipat : unit tactic = | IPatClear ids -> intro_clear (List.map Ssrcommon.hyp_id ids) future_ipats | IPatSimpl (Simpl n) -> - V82.tactic (Ssrequality.simpltac (Simpl n)) + V82.tactic ~nf_evars:false (Ssrequality.simpltac (Simpl n)) | IPatSimpl (Cut n) -> - V82.tactic (Ssrequality.simpltac (Cut n)) + V82.tactic ~nf_evars:false (Ssrequality.simpltac (Cut n)) | IPatSimpl (SimplCut (n,m)) -> - V82.tactic (Ssrequality.simpltac (SimplCut (n,m))) + V82.tactic ~nf_evars:false (Ssrequality.simpltac (SimplCut (n,m))) | IPatRewrite (occ,dir) -> Ssrcommon.tclWITHTOP - (fun x -> V82.tactic (Ssrequality.ipat_rewrite occ dir x)) + (fun x -> V82.tactic ~nf_evars:false (Ssrequality.ipat_rewrite occ dir x)) | IPatAbstractVars ids -> tclMK_ABSTRACT_VARS ids @@ -302,7 +302,7 @@ end let with_dgens { dgens; gens; clr } maintac = match gens with | [] -> with_defective maintac dgens clr | gen :: gens -> - V82.tactic (Ssrcommon.genstac (gens, clr)) <*> maintac dgens gen + V82.tactic ~nf_evars:false (Ssrcommon.genstac (gens, clr)) <*> maintac dgens gen let mkCoqEq env sigma = let eq = Coqlib.((build_coq_eq_data ()).eq) in @@ -326,7 +326,7 @@ let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr = | Term.ProdType (_, src, tgt) -> begin match EConstr.kind_of_type sigma src with | Term.AtomicType (hd, _) when Ssrcommon.is_protect hd env sigma -> - V82.tactic Ssrcommon.unprotecttac <*> + V82.tactic ~nf_evars:false Ssrcommon.unprotecttac <*> Ssrcommon.tclINTRO_ID ipat | _ -> Ssrcommon.tclINTRO_ANON <*> intro_eq () end @@ -380,9 +380,9 @@ let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr = | _ -> tclUNIT () in let unprot = if eqid <> None && is_rec - then V82.tactic Ssrcommon.unprotecttac else tclUNIT () in + then V82.tactic ~nf_evars:false Ssrcommon.unprotecttac else tclUNIT () in V82.of_tactic begin - V82.tactic ssrelim <*> + V82.tactic ~nf_evars:false ssrelim <*> tclIPAT_EQ (intro_eq <*> unprot) ipats end @@ -477,12 +477,12 @@ let ssrelimtac (view, (eqid, (dgens, ipats))) = | [v] -> Ssrcommon.tclINTERP_AST_CLOSURE_TERM_AS_CONSTR v >>= fun cs -> tclDISPATCH (List.map (fun elim -> - V82.tactic + V82.tactic ~nf_evars:false (Ssrelim.ssrelim deps (`EGen gen) ~elim eqid (elim_intro_tac ipats))) cs) | [] -> tclINDEPENDENT - (V82.tactic + (V82.tactic ~nf_evars:false (Ssrelim.ssrelim deps (`EGen gen) eqid (elim_intro_tac ipats))) | _ -> Ssrcommon.errorstrm @@ -497,7 +497,7 @@ let ssrcasetac (view, (eqid, (dgens, ipats))) = Ssrcommon.tacIS_INJECTION_CASE vc >>= fun inj -> let simple = (eqid = None && deps = [] && occ = None) in if simple && inj then - V82.tactic (Ssrelim.perform_injection vc) <*> + V82.tactic ~nf_evars:false (Ssrelim.perform_injection vc) <*> Tactics.clear (List.map Ssrcommon.hyp_id clear) <*> tclIPATssr ipats else @@ -506,7 +506,7 @@ let ssrcasetac (view, (eqid, (dgens, ipats))) = if view <> [] && eqid <> None && deps = [] then [gen], [], None else deps, clear, occ in - V82.tactic + V82.tactic ~nf_evars:false (Ssrelim.ssrelim ~is_case:true deps (`EConstr (clear, occ, vc)) eqid (elim_intro_tac ipats)) in @@ -515,7 +515,7 @@ let ssrcasetac (view, (eqid, (dgens, ipats))) = in with_dgens dgens (ndefectcasetac view eqid ipats) -let ssrscasetoptac = Ssrcommon.tclWITHTOP (Ssrelim.ssrscasetac false) +let ssrscasetoptac = Ssrcommon.tclWITHTOP Ssrelim.ssrscase_or_inj_tac let ssrselimtoptac = Ssrcommon.tclWITHTOP Ssrelim.elimtac (** [move] **************************************************************) @@ -555,7 +555,7 @@ let tclIPAT ip = let ssrmovetac = function | _::_ as view, (_, ({ gens = lastgen :: gens; clr }, ipats)) -> - let gentac = V82.tactic (Ssrcommon.genstac (gens, [])) in + let gentac = V82.tactic ~nf_evars:false (Ssrcommon.genstac (gens, [])) in let conclusion _ t clear ccl = Tactics.apply_type ~typecheck:true ccl [t] <*> Tactics.clear (List.map Ssrcommon.hyp_id clear) in @@ -569,7 +569,7 @@ let ssrmovetac = function let dgentac = with_dgens dgens eqmovetac in dgentac <*> tclIPAT (eqmoveipats pat ipats) | _, (_, ({ gens = (_ :: _ as gens); dgens = []; clr}, ipats)) -> - let gentac = V82.tactic (Ssrcommon.genstac (gens, clr)) in + let gentac = V82.tactic ~nf_evars:false (Ssrcommon.genstac (gens, clr)) in gentac <*> tclIPAT ipats | _, (_, ({ clr }, ipats)) -> Tacticals.New.tclTHENLIST [ssrsmovetac; Tactics.clear (List.map Ssrcommon.hyp_id clr); tclIPAT ipats] -- cgit v1.2.3