From 7721aeeede9c5578f29e7f37a5ea2005c7d9ce1b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 4 Apr 2018 11:16:59 +0200 Subject: [ssr] simplify delayed clears - we always rename - we compile {clear}/view to /view{clear} --- plugins/ssr/ssripats.ml | 44 ++++++++++++++++++++++++++++---------------- 1 file changed, 28 insertions(+), 16 deletions(-) (limited to 'plugins') diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 8207bc11e..09f3899ec 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -119,13 +119,10 @@ let intro_end = Ssrcommon.tcl0G (isCLR_CONSUME) (** [=> _] *****************************************************************) -let intro_clear ids future_ipats = +let intro_clear ids = Goal.enter begin fun gl -> let _, clear_ids, ren = List.fold_left (fun (used_ids, clear_ids, ren) id -> - if not(Ssrcommon.is_name_in_ipats id future_ipats) then begin - used_ids, id :: clear_ids, ren - end else let new_id = Ssrcommon.mk_anon_id (Id.to_string id) used_ids in (new_id :: used_ids, new_id :: clear_ids, (id, new_id) :: ren)) (Tacmach.New.pf_ids_of_hyps gl, [], []) ids @@ -213,22 +210,22 @@ let tclLOG p t = tclUNIT () end -let rec ipat_tac1 future_ipats ipat : unit tactic = +let rec ipat_tac1 ipat : unit tactic = match ipat with | IPatView l -> Ssrview.tclIPAT_VIEWS ~views:l - ~conclusion:(fun ~to_clear:clr -> intro_clear clr future_ipats) + ~conclusion:(fun ~to_clear:clr -> intro_clear clr) | IPatDispatch ipatss -> - tclEXTEND (List.map (ipat_tac future_ipats) ipatss) (tclUNIT ()) [] + tclEXTEND (List.map ipat_tac ipatss) (tclUNIT ()) [] | IPatId id -> Ssrcommon.tclINTRO_ID id | IPatCase ipatss -> - tclIORPAT (Ssrcommon.tclWITHTOP tac_case) future_ipats ipatss + tclIORPAT (Ssrcommon.tclWITHTOP tac_case) ipatss | IPatInj ipatss -> tclIORPAT (Ssrcommon.tclWITHTOP (fun t -> V82.tactic ~nf_evars:false (Ssrelim.perform_injection t))) - future_ipats ipatss + ipatss | IPatAnon Drop -> intro_drop | IPatAnon One -> Ssrcommon.tclINTRO_ANON @@ -239,7 +236,7 @@ let rec ipat_tac1 future_ipats ipat : unit tactic = | IPatClear ids -> tacCHECK_HYPS_EXIST ids <*> - intro_clear (List.map Ssrcommon.hyp_id ids) future_ipats + intro_clear (List.map Ssrcommon.hyp_id ids) | IPatSimpl (Simpl n) -> V82.tactic ~nf_evars:false (Ssrequality.simpltac (Simpl n)) @@ -256,17 +253,17 @@ let rec ipat_tac1 future_ipats ipat : unit tactic = | IPatTac t -> t -and ipat_tac future_ipats pl : unit tactic = +and ipat_tac pl : unit tactic = match pl with | [] -> tclUNIT () | pat :: pl -> - Ssrcommon.tcl0G (tclLOG pat (ipat_tac1 (pl @ future_ipats))) <*> + Ssrcommon.tcl0G (tclLOG pat ipat_tac1) <*> isTICK pat <*> - ipat_tac future_ipats pl + ipat_tac pl -and tclIORPAT tac future_ipats = function +and tclIORPAT tac = function | [[]] -> tac - | p -> Tacticals.New.tclTHENS tac (List.map (ipat_tac future_ipats) p) + | p -> Tacticals.New.tclTHENS tac (List.map ipat_tac p) let split_at_first_case ipats = let rec loop acc = function @@ -282,12 +279,27 @@ let ssr_exception is_on = function let option_to_list = function None -> [] | Some x -> [x] +(* Simple pass doing {x}/v -> /v{x} *) +let elaborate_ipats l = + let rec elab = function + | [] -> [] + | (IPatClear _ as p1) :: (IPatView _ as p2) :: rest -> p2 :: p1 :: elab rest + | IPatDispatch p :: rest -> IPatDispatch (List.map elab p) :: elab rest + | IPatCase p :: rest -> IPatCase (List.map elab p) :: elab rest + | IPatInj p :: rest -> IPatInj (List.map elab p) :: elab rest + | (IPatTac _ | IPatId _ | IPatSimpl _ | IPatClear _ | + IPatAnon _ | IPatView _ | IPatNoop | IPatRewrite _ | + IPatAbstractVars _) as x :: rest -> x :: elab rest + in + elab l + let main ?eqtac ~first_case_is_dispatch ipats = + let ipats = elaborate_ipats ipats in let ip_before, case, ip_after = split_at_first_case ipats in let case = ssr_exception first_case_is_dispatch case in let case = option_to_list case in let eqtac = option_to_list (Option.map (fun x -> IPatTac x) eqtac) in - Ssrcommon.tcl0G (ipat_tac [] (ip_before @ case @ eqtac @ ip_after) <*> intro_end) + Ssrcommon.tcl0G (ipat_tac (ip_before @ case @ eqtac @ ip_after) <*> intro_end) end (* }}} *) -- cgit v1.2.3 From a9dc951e9068b18ee1cf0e51b2c4ae7a7c40354a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 15 May 2018 13:39:08 +0200 Subject: [ssr] implement {}/v as a short hand for {v}/v when v is an id --- CHANGES | 6 +++ plugins/ssr/ssrast.mli | 2 +- plugins/ssr/ssripats.ml | 6 +-- plugins/ssr/ssrparser.ml4 | 19 +++++--- plugins/ssr/ssrprinters.ml | 3 +- plugins/ssr/ssrview.ml | 91 ++++++++++++++++++++++++--------------- plugins/ssr/ssrview.mli | 6 ++- test-suite/ssr/ipat_clear_if_id.v | 23 ++++++++++ 8 files changed, 110 insertions(+), 46 deletions(-) create mode 100644 test-suite/ssr/ipat_clear_if_id.v (limited to 'plugins') diff --git a/CHANGES b/CHANGES index 40626bf06..6ad2cc548 100644 --- a/CHANGES +++ b/CHANGES @@ -75,6 +75,12 @@ SSReflect In particular rule 3 lets one write {x}/v even if v uses the variable x: indeed the view is executed before the renaming. +- An empty clear switch is now accepted in intro patterns before a + view application whenever the view is a variable. + One can now write {}/v to mean {v}/v. Remark that {}/x is very similar + to the idiom {}e for the rewrite tactic (the equation e is used for + rewriting and then discarded). + Changes from 8.8.0 to 8.8.1 =========================== diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index 5571c5420..6ba937a2f 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -88,7 +88,7 @@ type ssripat = | IPatCase of (* ipats_mod option * *) ssripatss (* this is not equivalent to /case /[..|..] if there are already multiple goals *) | IPatInj of ssripatss | IPatRewrite of (*occurrence option * rewrite_pattern **) ssrocc * ssrdir - | IPatView of ssrview (* /view *) + | IPatView of bool * ssrview (* {}/view (true if the clear is present) *) | IPatClear of ssrclear (* {H1 H2} *) | IPatSimpl of ssrsimpl | IPatAbstractVars of Id.t list diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 09f3899ec..46fde4115 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -212,8 +212,8 @@ let tclLOG p t = let rec ipat_tac1 ipat : unit tactic = match ipat with - | IPatView l -> - Ssrview.tclIPAT_VIEWS ~views:l + | IPatView (clear_if_id,l) -> + Ssrview.tclIPAT_VIEWS ~views:l ~clear_if_id ~conclusion:(fun ~to_clear:clr -> intro_clear clr) | IPatDispatch ipatss -> tclEXTEND (List.map ipat_tac ipatss) (tclUNIT ()) [] @@ -588,7 +588,7 @@ let ssrmovetac = function (tacVIEW_THEN_GRAB view ~conclusion) <*> tclIPAT (IPatClear clr :: ipats) | _::_ as view, (_, ({ gens = []; clr }, ipats)) -> - tclIPAT (IPatView view :: IPatClear clr :: ipats) + tclIPAT (IPatView (false,view) :: IPatClear clr :: ipats) | _, (Some pat, (dgens, ipats)) -> let dgentac = with_dgens dgens eqmovetac in dgentac <*> tclIPAT (eqmoveipats pat ipats) diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 7a1d06fdc..347a1e4e2 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -412,8 +412,8 @@ let pr_docc = function let pr_ssrdocc _ _ _ = pr_docc ARGUMENT EXTEND ssrdocc TYPED AS ssrclear option * ssrocc PRINTED BY pr_ssrdocc -| [ "{" ne_ssrhyp_list(clr) "}" ] -> [ mkclr clr ] | [ "{" ssrocc(occ) "}" ] -> [ mkocc occ ] +| [ "{" ssrhyp_list(clr) "}" ] -> [ mkclr clr ] END (* Old kinds of terms *) @@ -578,7 +578,7 @@ let rec map_ipat map_id map_ssrhyp map_ast_closure_term = function | IPatCase iorpat -> IPatCase (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat) | IPatDispatch iorpat -> IPatDispatch (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat) | IPatInj iorpat -> IPatInj (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat) - | IPatView v -> IPatView (List.map map_ast_closure_term v) + | IPatView (clr,v) -> IPatView (clr,List.map map_ast_closure_term v) | IPatTac _ -> assert false (*internal usage only *) let wit_ssripatrep = add_genarg "ssripatrep" pr_ipat @@ -646,7 +646,7 @@ let interp_ipat ist gl = | IPatInj iorpat -> IPatInj (List.map (List.map interp) iorpat) | IPatAbstractVars l -> IPatAbstractVars (List.map get_intro_id (List.map (interp_introid ist gl) l)) - | IPatView l -> IPatView (List.map (fun x -> snd(interp_ast_closure_term ist + | IPatView (clr,l) -> IPatView (clr,List.map (fun x -> snd(interp_ast_closure_term ist gl x)) l) | (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop) as x -> x | IPatTac _ -> assert false (*internal usage only *) @@ -683,11 +683,17 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY pr_ssripats (* TODO | [ "+" ] -> [ [IPatAnon Temporary] ] *) | [ ssrsimpl_ne(sim) ] -> [ [IPatSimpl sim] ] | [ ssrdocc(occ) "->" ] -> [ match occ with + | Some [], _ -> CErrors.user_err ~loc (str"occ_switch expected") | None, occ -> [IPatRewrite (occ, L2R)] | Some clr, _ -> [IPatClear clr; IPatRewrite (allocc, L2R)]] | [ ssrdocc(occ) "<-" ] -> [ match occ with + | Some [], _ -> CErrors.user_err ~loc (str"occ_switch expected") | None, occ -> [IPatRewrite (occ, R2L)] | Some clr, _ -> [IPatClear clr; IPatRewrite (allocc, R2L)]] + | [ ssrdocc(occ) ssrfwdview(v) ] -> [ match occ with + | Some [], _ -> [IPatView (true,v)] + | Some cl, _ -> check_hyps_uniq [] cl; [IPatClear cl;IPatView (false,v)] + | _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here") ] | [ ssrdocc(occ) ] -> [ match occ with | Some cl, _ -> check_hyps_uniq [] cl; [IPatClear cl] | _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here")] @@ -705,7 +711,7 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY pr_ssripats | [ "-/" integer(n) "/=" ] -> [ [IPatNoop;IPatSimpl(SimplCut (n,~-1))] ] | [ "-/" integer(n) "/" integer (m) "=" ] -> [ [IPatNoop;IPatSimpl(SimplCut(n,m))] ] - | [ ssrfwdview(v) ] -> [ [IPatView v] ] + | [ ssrfwdview(v) ] -> [ [IPatView (false,v)] ] | [ "[" ":" ident_list(idl) "]" ] -> [ [IPatAbstractVars idl] ] | [ "[:" ident_list(idl) "]" ] -> [ [IPatAbstractVars idl] ] END @@ -1678,7 +1684,10 @@ let pr_gen (docc, dt) = pr_docc docc ++ pr_cpattern dt let pr_ssrgen _ _ _ = pr_gen ARGUMENT EXTEND ssrgen TYPED AS ssrdocc * cpattern PRINTED BY pr_ssrgen -| [ ssrdocc(docc) cpattern(dt) ] -> [ docc, dt ] +| [ ssrdocc(docc) cpattern(dt) ] -> [ + match docc with + | Some [], _ -> CErrors.user_err ~loc (str"Clear flag {} not allowed here") + | _ -> docc, dt ] | [ cpattern(dt) ] -> [ nodocc, dt ] END diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index 11369228c..8f4b2179e 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -107,7 +107,8 @@ let rec pr_ipat p = | IPatAnon All -> str "*" | IPatAnon Drop -> str "_" | IPatAnon One -> str "?" - | IPatView v -> pr_view2 v + | IPatView (false,v) -> pr_view2 v + | IPatView (true,v) -> str"{}" ++ pr_view2 v | IPatNoop -> str "-" | IPatAbstractVars l -> str "[:" ++ pr_list spc Id.print l ++ str "]" | IPatTac _ -> str "" diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index faebe3179..3f974ea06 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -67,9 +67,9 @@ end module State : sig (* View storage API *) - val vsINIT : EConstr.t -> unit tactic - val vsPUSH : (EConstr.t -> EConstr.t tactic) -> unit tactic - val vsCONSUME : (Id.t option -> EConstr.t -> unit tactic) -> unit tactic + val vsINIT : EConstr.t * Id.t list -> unit tactic + val vsPUSH : (EConstr.t -> (EConstr.t * Id.t list) tactic) -> unit tactic + val vsCONSUME : (name:Id.t option -> EConstr.t -> to_clear:Id.t list -> unit tactic) -> unit tactic val vsASSERT_EMPTY : unit tactic end = struct (* {{{ *) @@ -78,6 +78,7 @@ type vstate = { subject_name : Id.t option; (* top *) (* None if views are being applied to a term *) view : EConstr.t; (* v2 (v1 top) *) + to_clear : Id.t list; } include Ssrcommon.MakeState(struct @@ -85,13 +86,14 @@ include Ssrcommon.MakeState(struct let init = None end) -let vsINIT view = tclSET (Some { subject_name = None; view }) +let vsINIT (view, to_clear) = + tclSET (Some { subject_name = None; view; to_clear }) let vsPUSH k = tacUPDATE (fun s -> match s with - | Some { subject_name; view } -> - k view >>= fun view -> - tclUNIT (Some { subject_name; view }) + | Some { subject_name; view; to_clear } -> + k view >>= fun (view, clr) -> + tclUNIT (Some { subject_name; view; to_clear = to_clear @ clr }) | None -> Goal.enter_one ~__LOC__ begin fun gl -> let concl = Goal.concl gl in @@ -102,15 +104,15 @@ let vsPUSH k = | _ -> mk_anon_id "view_subject" (Tacmach.New.pf_ids_of_hyps gl) in let view = EConstr.mkVar id in Ssrcommon.tclINTRO_ID id <*> - k view >>= fun view -> - tclUNIT (Some { subject_name = Some id; view }) + k view >>= fun (view, to_clear) -> + tclUNIT (Some { subject_name = Some id; view; to_clear }) end) let vsCONSUME k = tclGET (fun s -> match s with - | Some { subject_name; view } -> + | Some { subject_name; view; to_clear } -> tclSET None <*> - k subject_name view + k ~name:subject_name view ~to_clear | None -> anomaly "vsCONSUME: empty storage") let vsASSERT_EMPTY = @@ -187,6 +189,16 @@ end * modular, see the 2 functions below that would need to "uncommit" *) let tclKeepOpenConstr (_env, sigma, t) = Unsafe.tclEVARS sigma <*> tclUNIT t +let tclADD_CLEAR_IF_ID (env, ist, t) x = + Ssrprinters.ppdebug (lazy + Pp.(str"tclADD_CLEAR_IF_ID: " ++ Printer.pr_econstr_env env ist t)); + let hd, _ = EConstr.decompose_app ist t in + match EConstr.kind ist hd with + | Constr.Var id when Ssrcommon.not_section_id id -> tclUNIT (x, [id]) + | _ -> tclUNIT (x,[]) + +let tclPAIR p x = tclUNIT (x, p) + (* The ssr heuristic : *) (* Estimate a bound on the number of arguments of a raw constr. *) (* This is not perfect, because the unifier may fail to *) @@ -203,14 +215,15 @@ let guess_max_implicits ist glob = (fun _ -> tclUNIT 5) let pad_to_inductive ist glob = Goal.enter_one ~__LOC__ begin fun goal -> - interp_glob ist glob >>= fun (env, sigma, term) -> + interp_glob ist glob >>= fun (env, sigma, term as ot) -> let term_ty = Retyping.get_type_of env sigma term in let ctx, i = Reductionops.splay_prod env sigma term_ty in let rel_ctx = List.map (fun (a,b) -> Context.Rel.Declaration.LocalAssum(a,b)) ctx in - if Ssrcommon.isAppInd (EConstr.push_rel_context rel_ctx env) sigma i - then tclUNIT (mkGApp glob (mkGHoles (List.length ctx))) - else Tacticals.New.tclZEROMSG Pp.(str"not an inductive") + if not (Ssrcommon.isAppInd (EConstr.push_rel_context rel_ctx env) sigma i) + then Tacticals.New.tclZEROMSG Pp.(str"not an inductive") + else tclUNIT (mkGApp glob (mkGHoles (List.length ctx))) + >>= tclADD_CLEAR_IF_ID ot end (* There are two ways of "applying" a view to term: *) @@ -221,7 +234,7 @@ end (* They require guessing the view hints and the number of *) (* implicits, respectively, which we do by brute force. *) (* Builds v p *) -let interp_view ist v p = +let interp_view ~clear_if_id ist v p = let is_specialize hd = match DAst.get hd with Glob_term.GHole _ -> true | _ -> false in (* We cast the pile of views p into a term p_id *) @@ -230,25 +243,31 @@ let interp_view ist v p = match DAst.get v with | Glob_term.GApp (hd, rargs) when is_specialize hd -> Ssrprinters.ppdebug (lazy Pp.(str "specialize")); - interp_glob ist (mkGApp p_id rargs) >>= tclKeepOpenConstr + interp_glob ist (mkGApp p_id rargs) + >>= tclKeepOpenConstr >>= tclPAIR [] | _ -> Ssrprinters.ppdebug (lazy Pp.(str "view")); (* We find out how to build (v p) eventually using an adaptor *) let adaptors = AdaptorDb.(get Forward) in Proofview.tclORELSE - (pad_to_inductive ist v >>= fun vpad -> + (pad_to_inductive ist v >>= fun (vpad,clr) -> Ssrcommon.tclFIRSTa (List.map - (fun a -> interp_glob ist (mkGApp a [vpad; p_id])) adaptors)) + (fun a -> interp_glob ist (mkGApp a [vpad; p_id])) adaptors) + >>= tclPAIR clr) (fun _ -> guess_max_implicits ist v >>= fun n -> Ssrcommon.tclFIRSTi (fun n -> - interp_glob ist (mkGApp v (mkGHoles n @ [p_id]))) n) - >>= tclKeepOpenConstr + interp_glob ist (mkGApp v (mkGHoles n @ [p_id]))) n + >>= fun x -> tclADD_CLEAR_IF_ID x x) + >>= fun (ot,clr) -> + if clear_if_id + then tclKeepOpenConstr ot >>= tclPAIR clr + else tclKeepOpenConstr ot >>= tclPAIR [] (* we store in the state (v top), then (v1 (v2 top))... *) -let pile_up_view (ist, v) = +let pile_up_view ~clear_if_id (ist, v) = let ist = Ssrcommon.option_assert_get ist (Pp.str"not a term") in - State.vsPUSH (fun p -> interp_view ist v p) + State.vsPUSH (fun p -> interp_view ~clear_if_id ist v p) let finalize_view s0 ?(simple_types=true) p = Goal.enter_one ~__LOC__ begin fun g -> @@ -292,7 +311,7 @@ let pose_proof subject_name p = <*> Tactics.New.reduce_after_refine -let rec apply_all_views ending vs s0 = +let rec apply_all_views ~clear_if_id ending vs s0 = match vs with | [] -> ending s0 | v :: vs -> @@ -301,31 +320,35 @@ let rec apply_all_views ending vs s0 = | `Tac tac -> Ssrprinters.ppdebug (lazy Pp.(str"..a tactic")); ending s0 <*> Tacinterp.eval_tactic tac <*> - Ssrcommon.tacSIGMA >>= apply_all_views ending vs + Ssrcommon.tacSIGMA >>= apply_all_views ~clear_if_id ending vs | `Term v -> Ssrprinters.ppdebug (lazy Pp.(str"..a term")); - pile_up_view v <*> apply_all_views ending vs s0 + pile_up_view ~clear_if_id v <*> + apply_all_views ~clear_if_id ending vs s0 (* Entry points *********************************************************) -let tclIPAT_VIEWS ~views:vs ~conclusion:tac = +let tclIPAT_VIEWS ~views:vs ?(clear_if_id=false) ~conclusion:tac = let end_view_application s0 = - State.vsCONSUME (fun name t -> - finalize_view s0 t >>= pose_proof name <*> - tac ~to_clear:(Option.cata (fun x -> [x]) [] name)) in + State.vsCONSUME (fun ~name t ~to_clear -> + let to_clear = Option.cata (fun x -> [x]) [] name @ to_clear in + finalize_view s0 t >>= pose_proof name <*> tac ~to_clear) in tclINDEPENDENT begin State.vsASSERT_EMPTY <*> - Ssrcommon.tacSIGMA >>= apply_all_views end_view_application vs <*> + Ssrcommon.tacSIGMA >>= + apply_all_views ~clear_if_id end_view_application vs <*> State.vsASSERT_EMPTY end let tclWITH_FWD_VIEWS ~simple_types ~subject ~views:vs ~conclusion:tac = let ending_tac s0 = - State.vsCONSUME (fun _ t -> finalize_view s0 ~simple_types t >>= tac) in + State.vsCONSUME (fun ~name:_ t ~to_clear:_ -> + finalize_view s0 ~simple_types t >>= tac) in tclINDEPENDENT begin State.vsASSERT_EMPTY <*> - State.vsINIT subject <*> - Ssrcommon.tacSIGMA >>= apply_all_views ending_tac vs <*> + State.vsINIT (subject,[]) <*> + Ssrcommon.tacSIGMA >>= + apply_all_views ~clear_if_id:false ending_tac vs <*> State.vsASSERT_EMPTY end diff --git a/plugins/ssr/ssrview.mli b/plugins/ssr/ssrview.mli index be51fe7f9..b128a95da 100644 --- a/plugins/ssr/ssrview.mli +++ b/plugins/ssr/ssrview.mli @@ -20,9 +20,11 @@ module AdaptorDb : sig end -(* Apply views to the top of the stack (intro pattern) *) +(* Apply views to the top of the stack (intro pattern). If clear_if_id is + * true (default false) then views that happen to be a variable are considered + * as to be cleared (see the to_clear argument to the continuation) *) val tclIPAT_VIEWS : - views:ast_closure_term list -> + views:ast_closure_term list -> ?clear_if_id:bool -> conclusion:(to_clear:Names.Id.t list -> unit Proofview.tactic) -> unit Proofview.tactic diff --git a/test-suite/ssr/ipat_clear_if_id.v b/test-suite/ssr/ipat_clear_if_id.v new file mode 100644 index 000000000..7a44db2ea --- /dev/null +++ b/test-suite/ssr/ipat_clear_if_id.v @@ -0,0 +1,23 @@ +Require Import ssreflect. + +Axiom v1 : nat -> bool. + +Section Foo. + +Variable v2 : nat -> bool. + +Lemma test (v3 : nat -> bool) (v4 : bool -> bool) (v5 : bool -> bool) : nat -> nat -> nat -> nat -> True. +Proof. +move=> {}/v1 b1 {}/v2 b2 {}/v3 b3 {}/v2/v4/v5 b4. +Check b1 : bool. +Check b2 : bool. +Check b3 : bool. +Check b4 : bool. +Fail Check v3. +Fail Check v4. +Fail Check v5. +Check v2 : nat -> bool. +by []. +Qed. + +End Foo. -- cgit v1.2.3