diff options
29 files changed, 1237 insertions, 26 deletions
diff --git a/doc/changelog/04-tactics/12129-add-with-strategy.rst b/doc/changelog/04-tactics/12129-add-with-strategy.rst new file mode 100644 index 0000000000..68558c0cf4 --- /dev/null +++ b/doc/changelog/04-tactics/12129-add-with-strategy.rst @@ -0,0 +1,4 @@ +- **Added:** + New tactical :tacn:`with_strategy` added which behaves like the + command :cmd:`Strategy`, with effects local to the given tactic + (`#12129 <https://github.com/coq/coq/pull/12129>`_, by Jason Gross). diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 8989dd29ab..fd6b2b3846 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3355,6 +3355,26 @@ the conversion in hypotheses :n:`{+ @ident}`. This is the most general syntax that combines the different variants. +.. tacn:: with_strategy @strategy_level_or_var [ {+ @smart_qualid } ] @ltac_expr3 + :name: with_strategy + + Executes :token:`ltac_expr3`, applying the alternate unfolding + behavior that the :cmd:`Strategy` command controls, but only for + :token:`ltac_expr3`. This can be useful for guarding calls to + reduction in tactic automation to ensure that certain constants are + never unfolded by tactics like :tacn:`simpl` and :tacn:`cbn` or to + ensure that unfolding does not fail. + + .. note:: + + Use this tactic with care, as effects do not persist past the + end of the proof script. Notably, this fine-tuning of the + conversion strategy is not in effect during :cmd:`Qed` nor + :cmd:`Defined`, so this tactic is most useful to guard + calls to conversion in tactic automation to ensure that, e.g., + :tacn:`unfold` does not fail just because the user made a + constant :cmd:`Opaque`. + Conversion tactics applied to hypotheses ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 1759264e87..7191444bac 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -817,13 +817,15 @@ described first. .. cmd:: Strategy {+ @strategy_level [ {+ @smart_qualid } ] } - .. insertprodn strategy_level strategy_level + .. insertprodn strategy_level strategy_level_or_var .. prodn:: strategy_level ::= opaque | @int | expand | transparent + strategy_level_or_var ::= @strategy_level + | @ident This command accepts the :attr:`local` attribute, which limits its effect to the current section or module, in which case the section and module diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index d72409e0d9..ea5ad79a80 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1714,6 +1714,11 @@ Tactic notations allow customizing the syntax of tactics. - a global reference of term - :tacn:`unfold` + * - ``smart_global`` + - :token:`smart_qualid` + - a global reference of term + - :tacn:`with_strategy` + * - ``constr`` - :token:`term` - a term @@ -1734,6 +1739,16 @@ Tactic notations allow customizing the syntax of tactics. - an integer - :tacn:`do` + * - ``strategy_level`` + - :token:`strategy_level` + - a strategy level + - + + * - ``strategy_level_or_var`` + - :token:`strategy_level_or_var` + - a strategy level + - :tacn:`with_strategy` + * - ``tactic`` - :token:`ltac_expr` - a tactic @@ -1766,18 +1781,24 @@ Tactic notations allow customizing the syntax of tactics. .. todo: notation doesn't support italics - .. note:: In order to be bound in tactic definitions, each syntactic - entry for argument type must include the case of a simple |Ltac| - identifier as part of what it parses. This is naturally the case for - ``ident``, ``simple_intropattern``, ``reference``, ``constr``, ... but not for ``integer``. - This is the reason for introducing a special entry ``int_or_var`` which - evaluates to integers only but which syntactically includes + .. note:: In order to be bound in tactic definitions, each + syntactic entry for argument type must include the case + of a simple |Ltac| identifier as part of what it + parses. This is naturally the case for ``ident``, + ``simple_intropattern``, ``reference``, ``constr``, ... + but not for ``integer`` nor for ``strategy_level``. This + is the reason for introducing special entries + ``int_or_var`` and ``strategy_level_or_var`` which + evaluate to integers or strategy levels only, + respectively, but which syntactically includes identifiers in order to be usable in tactic definitions. - .. note:: The *entry*\ ``_list*`` and ``ne_``\ *entry*\ ``_list*`` entries can be used in - primitive tactics or in other notations at places where a list of the - underlying entry can be used: entry is either ``constr``, ``hyp``, ``integer`` - or ``int_or_var``. + .. note:: The *entry*\ ``_list*`` and ``ne_``\ *entry*\ ``_list*`` + entries can be used in primitive tactics or in other + notations at places where a list of the underlying entry + can be used: entry is either ``constr``, ``hyp``, + ``integer``, ``smart_qualid``, ``strategy_level``, + ``strategy_level_or_var``, or ``int_or_var``. .. rubric:: Footnotes diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index c7e3ee18ad..62cc8ea86b 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1839,3 +1839,7 @@ sentence: [ document: [ | LIST0 sentence ] + +strategy_level: [ +| DELETE strategy_level0 +] diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 4274dccb40..92e9df51d5 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -451,6 +451,14 @@ bar_cbrace: [ | test_pipe_closedcurly "|" "}" ] +strategy_level: [ +| "expand" +| "opaque" +| integer +| "transparent" +| strategy_level0 +] + vernac_toplevel: [ | "Drop" "." | "Quit" "." @@ -1213,13 +1221,6 @@ more_implicits_block: [ | "{" LIST1 name "}" ] -strategy_level: [ -| "expand" -| "opaque" -| integer -| "transparent" -] - instance_name: [ | ident_decl binders | @@ -1598,6 +1599,7 @@ simple_tactic: [ | "guard" test | "decompose" "[" LIST1 constr "]" constr | "optimize_heap" +| "with_strategy" strategy_level_or_var "[" LIST1 smart_global "]" tactic3 | "eassumption" | "eexact" constr | "trivial" auto_using hintbases @@ -1855,6 +1857,11 @@ test_lpar_id_colon: [ | local_test_lpar_id_colon ] +strategy_level_or_var: [ +| strategy_level +| identref +] + comparison: [ | "=" | "<" diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index df4e5a22e3..11f06b7b8a 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -659,6 +659,11 @@ strategy_level: [ | "transparent" ] +strategy_level_or_var: [ +| strategy_level +| ident +] + reserv_list: [ | LIST1 ( "(" simple_reserv ")" ) | simple_reserv @@ -1234,6 +1239,7 @@ simple_tactic: [ | "guard" int_or_var comparison int_or_var | "decompose" "[" LIST1 one_term "]" one_term | "optimize_heap" +| "with_strategy" strategy_level_or_var "[" LIST1 smart_qualid "]" ltac_expr3 | "start" "ltac" "profiling" | "stop" "ltac" "profiling" | "reset" "ltac" "profile" diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 492671fff0..d5f104b7f8 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -42,6 +42,8 @@ let wit_var = let wit_ref = make0 "ref" +let wit_smart_global = make0 ~dyn:(val_tag (topwit wit_ref)) "smart_global" + let wit_sort_family = make0 "sort_family" let wit_constr = diff --git a/interp/stdarg.mli b/interp/stdarg.mli index 35de3693cb..89bdd78c70 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -39,6 +39,8 @@ val wit_var : (lident, lident, Id.t) genarg_type val wit_ref : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type +val wit_smart_global : (qualid or_by_notation, GlobRef.t located or_var, GlobRef.t) genarg_type + val wit_sort_family : (Sorts.family, unit, unit) genarg_type val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 9b87c194c5..3ee1d2fb1f 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -19,6 +19,12 @@ open Names * The default value is [Level 100]. *) type level = Expand | Level of int | Opaque +let pr_level = function + | Expand -> Pp.str "expand" + | Level 0 -> Pp.str "transparent" + | Level n -> Pp.int n + | Opaque -> Pp.str "opaque" + let default = Level 0 let is_default = function | Level 0 -> true diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli index b25488d94a..930edf6c49 100644 --- a/kernel/conv_oracle.mli +++ b/kernel/conv_oracle.mli @@ -27,6 +27,7 @@ val oracle_order : ('a -> Constant.t) -> oracle -> bool -> * The default value (transparent constants) is [Level 0]. *) type level = Expand | Level of int | Opaque +val pr_level : level -> Pp.t val transparent : level (** Check whether a level is transparent *) @@ -42,4 +43,3 @@ val set_strategy : oracle -> Constant.t tableKey -> level -> oracle val fold_strategy : (Constant.t tableKey -> level -> 'a -> 'a) -> oracle -> 'a -> 'a val get_transp_state : oracle -> TransparentState.t - diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg index 9c50109bb3..7cabd850ad 100644 --- a/parsing/g_prim.mlg +++ b/parsing/g_prim.mlg @@ -53,7 +53,7 @@ GRAMMAR EXTEND Gram bignat bigint natural integer identref name ident var preident fullyqualid qualid reference dirpath ne_lstring ne_string string lstring pattern_ident pattern_identref by_notation - smart_global bar_cbrace; + smart_global bar_cbrace strategy_level; preident: [ [ s = IDENT -> { s } ] ] ; @@ -140,4 +140,10 @@ GRAMMAR EXTEND Gram bar_cbrace: [ [ test_pipe_closedcurly; "|"; "}" -> { () } ] ] ; + strategy_level: + [ [ IDENT "expand" -> { Conv_oracle.Expand } + | IDENT "opaque" -> { Conv_oracle.Opaque } + | n=integer -> { Conv_oracle.Level n } + | IDENT "transparent" -> { Conv_oracle.transparent } ] ] + ; END diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 5b0562fb0d..2cc16f85d5 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -276,6 +276,7 @@ module Prim = let reference = make_gen_entry uprim "reference" let by_notation = Entry.create "by_notation" let smart_global = Entry.create "smart_global" + let strategy_level = gec_gen "strategy_level" (* parsed like ident but interpreted as a term *) let var = gec_gen "var" @@ -505,6 +506,7 @@ let () = Grammar.register0 wit_ident (Prim.ident); Grammar.register0 wit_var (Prim.var); Grammar.register0 wit_ref (Prim.reference); + Grammar.register0 wit_smart_global (Prim.smart_global); Grammar.register0 wit_sort_family (Constr.sort_family); Grammar.register0 wit_constr (Constr.constr); () diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 90088be307..bd64d21518 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -170,6 +170,7 @@ module Prim : val ne_lstring : lstring Entry.t val var : lident Entry.t val bar_cbrace : unit Entry.t + val strategy_level : Conv_oracle.level Entry.t end module Constr : diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index c4731e5c34..eb53fd45d0 100644 --- a/plugins/ltac/extraargs.mlg +++ b/plugins/ltac/extraargs.mlg @@ -31,6 +31,8 @@ let create_generic_quotation name e wit = let () = create_generic_quotation "integer" Pcoq.Prim.integer Stdarg.wit_int let () = create_generic_quotation "string" Pcoq.Prim.string Stdarg.wit_string +let () = create_generic_quotation "smart_global" Pcoq.Prim.smart_global Stdarg.wit_smart_global + let () = create_generic_quotation "ident" Pcoq.Prim.ident Stdarg.wit_ident let () = create_generic_quotation "reference" Pcoq.Prim.reference Stdarg.wit_ref let () = create_generic_quotation "uconstr" Pcoq.Constr.lconstr Stdarg.wit_uconstr @@ -342,3 +344,55 @@ let pr_lpar_id_colon _ _ _ _ = mt () ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY { pr_lpar_id_colon } | [ local_test_lpar_id_colon(x) ] -> { () } END + +{ + +(* Work around a limitation of the macro system *) +let strategy_level0 = Pcoq.Prim.strategy_level + +let pr_strategy _ _ _ v = Conv_oracle.pr_level v + +} + +ARGUMENT EXTEND strategy_level PRINTED BY { pr_strategy } +| [ strategy_level0(n) ] -> { n } +END + +{ + +let intern_strategy ist v = match v with +| ArgVar id -> ArgVar (Tacintern.intern_hyp ist id) +| ArgArg v -> ArgArg v + +let subst_strategy _ v = v + +let interp_strategy ist gl = function +| ArgArg n -> gl.Evd.sigma, n +| ArgVar { CAst.v = id; CAst.loc } -> + let v = + try Id.Map.find id ist.lfun + with Not_found -> + CErrors.user_err ?loc + (str "Unbound variable " ++ Id.print id ++ str".") + in + let v = + try Tacinterp.Value.cast (Genarg.topwit wit_strategy_level) v + with CErrors.UserError _ -> Taccoerce.error_ltac_variable ?loc id None v "a strategy_level" + in + gl.Evd.sigma, v + +let pr_loc_strategy _ _ _ v = Pputils.pr_or_var Conv_oracle.pr_level v + +} + +ARGUMENT EXTEND strategy_level_or_var + TYPED AS strategy_level + PRINTED BY { pr_strategy } + INTERPRETED BY { interp_strategy } + GLOBALIZED BY { intern_strategy } + SUBSTITUTED BY { subst_strategy } + RAW_PRINTED BY { pr_loc_strategy } + GLOB_PRINTED BY { pr_loc_strategy } +| [ strategy_level(n) ] -> { ArgArg n } +| [ identref(id) ] -> { ArgVar id } +END diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index fbdb7c0032..e52bf55f71 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -78,3 +78,7 @@ val wit_in_clause : (lident Locus.clause_expr, lident Locus.clause_expr, Id.t Locus.clause_expr) Genarg.genarg_type + +val wit_strategy_level : Conv_oracle.level Genarg.uniform_genarg_type + +val wit_strategy_level_or_var : (Conv_oracle.level Locus.or_var, Conv_oracle.level Locus.or_var, Conv_oracle.level) Genarg.genarg_type diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 0bad3cbe5b..ffb597d4cb 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -1119,3 +1119,11 @@ let tclOPTIMIZE_HEAP = TACTIC EXTEND optimize_heap | [ "optimize_heap" ] -> { tclOPTIMIZE_HEAP } END + +(** Tactic analogous to [Strategy] vernacular *) + +TACTIC EXTEND with_strategy +| [ "with_strategy" strategy_level_or_var(v) "[" ne_smart_global_list(q) "]" tactic3(tac) ] -> { + with_set_strategy [(v, q)] (Tacinterp.tactic_of_value ist tac) +} +END diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 09f1fc371a..d74e981c6d 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1325,6 +1325,8 @@ let () = register_basic_print0 wit_int_or_var (pr_or_var int) (pr_or_var int) int; register_basic_print0 wit_ref pr_qualid (pr_or_var (pr_located pr_global)) pr_global; + register_basic_print0 wit_smart_global + (pr_or_by_notation pr_qualid) (pr_or_var (pr_located pr_global)) pr_global; register_basic_print0 wit_ident pr_id pr_id pr_id; register_basic_print0 wit_var pr_lident pr_lident pr_id; register_print0 wit_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env [@warning "-3"]; diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 04d85ed390..91d26519b8 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -293,6 +293,13 @@ let coerce_to_evaluable_ref env sigma v = | VarRef var -> EvalVarRef var | ConstRef c -> EvalConstRef c | IndRef _ | ConstructRef _ -> fail () + else if has_type v (topwit wit_smart_global) then + let open GlobRef in + let r = out_gen (topwit wit_smart_global) v in + match r with + | VarRef var -> EvalVarRef var + | ConstRef c -> EvalConstRef c + | IndRef _ | ConstructRef _ -> fail () else match Value.to_constr v with | Some c when isConst sigma c -> EvalConstRef (fst (destConst sigma c)) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 597c3fdaac..929fd5e132 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -305,6 +305,12 @@ let intern_evaluable_reference_or_by_notation ist = function (Notation.interp_notation_as_global_reference ?loc GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc) +let intern_smart_global ist = function + | {v=AN r} -> intern_global_reference ist r + | {v=ByNotation (ntn,sc);loc} -> + ArgArg (loc, (Notation.interp_notation_as_global_reference ?loc + GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)) + (* Globalize a reduction expression *) let intern_evaluable ist r = let f ist r = @@ -813,6 +819,7 @@ let intern_ltac ist tac = let () = Genintern.register_intern0 wit_int_or_var (lift intern_int_or_var); + Genintern.register_intern0 wit_smart_global (lift intern_smart_global); Genintern.register_intern0 wit_ref (lift intern_global_reference); Genintern.register_intern0 wit_pre_ident (fun ist c -> (ist,c)); Genintern.register_intern0 wit_ident intern_ident'; diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 6debc7d9b9..d1f031b418 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -2022,6 +2022,7 @@ let interp_pre_ident ist env sigma s = let () = register_interp0 wit_int_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n)); + register_interp0 wit_smart_global (lift interp_reference); register_interp0 wit_ref (lift interp_reference); register_interp0 wit_pre_ident (lift interp_pre_ident); register_interp0 wit_ident (lift interp_ident); diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 600c30b403..ed298b7e66 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -280,6 +280,7 @@ and subst_genarg subst (GenArg (Glbwit wit, x)) = let () = Genintern.register_subst0 wit_int_or_var (fun _ v -> v); Genintern.register_subst0 wit_ref subst_global_reference; + Genintern.register_subst0 wit_smart_global subst_global_reference; Genintern.register_subst0 wit_pre_ident (fun _ v -> v); Genintern.register_subst0 wit_ident (fun _ v -> v); Genintern.register_subst0 wit_var (fun _ v -> v); diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e4809332c5..b17f02f224 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -5045,6 +5045,29 @@ let unify ?(state=TransparentState.full) x y = Proofview.tclZERO (PretypeError (env, sigma, CannotUnify (x, y, None))) end +let with_set_strategy lvl_ql k = + let glob_key r = + match r with + | GlobRef.ConstRef sp -> ConstKey sp + | GlobRef.VarRef id -> VarKey id + | _ -> user_err Pp.(str + "cannot set an inductive type or a constructor as transparent") in + let kl = List.concat (List.map (fun (lvl, ql) -> List.map (fun q -> (lvl, glob_key q)) ql) lvl_ql) in + Proofview.tclENV >>= fun env -> + let orig_kl = List.map (fun (_lvl, k) -> + (Conv_oracle.get_strategy (Environ.oracle env) k, k)) + kl in + let env = List.fold_left (fun env (lvl, k) -> + Environ.set_oracle env + (Conv_oracle.set_strategy (Environ.oracle env) k lvl)) env kl in + Proofview.Unsafe.tclSETENV env <*> + k <*> + Proofview.tclENV >>= fun env -> + let env = List.fold_left (fun env (lvl, k) -> + Environ.set_oracle env + (Conv_oracle.set_strategy (Environ.oracle env) k lvl)) env orig_kl in + Proofview.Unsafe.tclSETENV env + module Simple = struct (** Simplified version of some of the above tactics *) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index c84ba17f23..fb4367f3aa 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -435,6 +435,12 @@ val declare_intro_decomp_eq : (types * constr * constr) -> constr * types -> unit Proofview.tactic) -> unit +(** Tactic analogous to the [Strategy] vernacular, but only applied + locally to the tactic argument *) +val with_set_strategy : + (Conv_oracle.level * Names.GlobRef.t list) list -> + unit Proofview.tactic -> unit Proofview.tactic + (** {6 Simple form of basic tactics. } *) module Simple : sig diff --git a/test-suite/output/print_ltac.out b/test-suite/output/print_ltac.out index 952761acca..58931c4b82 100644 --- a/test-suite/output/print_ltac.out +++ b/test-suite/output/print_ltac.out @@ -6,3 +6,340 @@ Ltac t3 := idtacstr "my tactic" Ltac t4 x := match x with | ?A => (A, A) end +The command has indeed failed with message: +idnat is bound to a notation that does not denote a reference. +Ltac withstrategy l x := + let idx := smart_global:(id) in + let tl := strategy_level:(transparent) in + with_strategy + 1 + [ + id + id + ] + with_strategy + l + [ + id + id + ] + with_strategy + tl + [ + id + id + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + opaque + [ + id + id + ] + with_strategy + expand + [ + id + id + ] + with_strategy + transparent + [ + idx + ] + with_strategy + transparent + [ + id + x + ] + with_strategy + transparent + [ + x + id + ] + with_strategy + transparent + [ + id + ] + with_strategy + transparent + [ + id + x + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + transparent + [ + id + id + x + ] + with_strategy + transparent + [ + id + ] + with_strategy + transparent + [ + id + x + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + transparent + [ + id + id + x + ] + idtac +The command has indeed failed with message: +idnat is bound to a notation that does not denote a reference. +Ltac withstrategy l x := + let idx := smart_global:(id) in + let tl := strategy_level:(transparent) in + with_strategy + 1 + [ + id + id + ] + with_strategy + l + [ + id + id + ] + with_strategy + tl + [ + id + id + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + opaque + [ + id + id + ] + with_strategy + expand + [ + id + id + ] + with_strategy + transparent + [ + idx + ] + with_strategy + transparent + [ + id + x + ] + with_strategy + transparent + [ + x + id + ] + with_strategy + transparent + [ + id + ] + with_strategy + transparent + [ + id + x + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + transparent + [ + id + id + x + ] + with_strategy + transparent + [ + id + ] + with_strategy + transparent + [ + id + x + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + transparent + [ + id + id + x + ] + idtac +Ltac FE.withstrategy l x := + let idx := smart_global:(FE.id) in + let tl := strategy_level:(transparent) in + with_strategy + 1 + [ + FE.id + FE.id + ] + with_strategy + l + [ + FE.id + FE.id + ] + with_strategy + tl + [ + FE.id + FE.id + ] + with_strategy + transparent + [ + FE.id + FE.id + ] + with_strategy + transparent + [ + FE.id + FE.id + ] + with_strategy + opaque + [ + FE.id + FE.id + ] + with_strategy + expand + [ + FE.id + FE.id + ] + with_strategy + transparent + [ + idx + ] + with_strategy + transparent + [ + FE.id + x + ] + with_strategy + transparent + [ + x + FE.id + ] + with_strategy + transparent + [ + FE.id + ] + with_strategy + transparent + [ + FE.id + x + ] + with_strategy + transparent + [ + FE.id + FE.id + ] + with_strategy + transparent + [ + FE.id + FE.id + x + ] + with_strategy + transparent + [ + FE.id + ] + with_strategy + transparent + [ + FE.id + x + ] + with_strategy + transparent + [ + FE.id + FE.id + ] + with_strategy + transparent + [ + FE.id + FE.id + x + ] + idtac diff --git a/test-suite/output/print_ltac.v b/test-suite/output/print_ltac.v index a992846791..d0883e32e4 100644 --- a/test-suite/output/print_ltac.v +++ b/test-suite/output/print_ltac.v @@ -10,3 +10,73 @@ Print Ltac t3. (* https://github.com/coq/coq/issues/9716 *) Ltac t4 x := match x with ?A => constr:((A, A)) end. Print Ltac t4. + +Notation idnat := (@id nat). +Notation idn := id. +Notation idan := (@id). +Fail Strategy transparent [idnat]. +Strategy transparent [idn]. +Strategy transparent [idan]. +Ltac withstrategy l x := + let idx := smart_global:(id) in + let tl := strategy_level:(transparent) in + with_strategy 1 [id id] ( + with_strategy l [id id] ( + with_strategy tl [id id] ( + with_strategy 0 [id id] ( + with_strategy transparent [id id] ( + with_strategy opaque [id id] ( + with_strategy expand [id id] ( + with_strategy 0 [idx] ( + with_strategy 0 [id x] ( + with_strategy 0 [x id] ( + with_strategy 0 [idn] ( + with_strategy 0 [idn x] ( + with_strategy 0 [idn id] ( + with_strategy 0 [idn id x] ( + with_strategy 0 [idan] ( + with_strategy 0 [idan x] ( + with_strategy 0 [idan id] ( + with_strategy 0 [idan id x] ( + idtac + )))))))))))))))))). +Print Ltac withstrategy. + +Module Type Empty. End Empty. +Module E. End E. +Module F (E : Empty). + Definition id {T} := @id T. + Notation idnat := (@id nat). + Notation idn := id. + Notation idan := (@id). + Fail Strategy transparent [idnat]. + Strategy transparent [idn]. + Strategy transparent [idan]. + Ltac withstrategy l x := + let idx := smart_global:(id) in + let tl := strategy_level:(transparent) in + with_strategy 1 [id id] ( + with_strategy l [id id] ( + with_strategy tl [id id] ( + with_strategy 0 [id id] ( + with_strategy transparent [id id] ( + with_strategy opaque [id id] ( + with_strategy expand [id id] ( + with_strategy 0 [idx] ( + with_strategy 0 [id x] ( + with_strategy 0 [x id] ( + with_strategy 0 [idn] ( + with_strategy 0 [idn x] ( + with_strategy 0 [idn id] ( + with_strategy 0 [idn id x] ( + with_strategy 0 [idan] ( + with_strategy 0 [idan x] ( + with_strategy 0 [idan id] ( + with_strategy 0 [idan id x] ( + idtac + )))))))))))))))))). + Print Ltac withstrategy. +End F. + +Module FE := F E. +Print Ltac FE.withstrategy. diff --git a/test-suite/success/strategy.v b/test-suite/success/strategy.v new file mode 100644 index 0000000000..926ba54342 --- /dev/null +++ b/test-suite/success/strategy.v @@ -0,0 +1,87 @@ +Notation aid := (@id) (only parsing). +Notation idn := id (only parsing). +Ltac unfold_id := unfold id. + +Fixpoint fact (n : nat) + := match n with + | 0 => 1 + | S n => (S n) * fact n + end. + +Opaque id. +Goal id (fact 100) = fact 100. + Strategy expand [id]. + Time Timeout 5 reflexivity. (* should be instant *) + (* Finished transaction in 0. secs (0.u,0.s) (successful) *) +Time Timeout 5 Defined. +(* Finished transaction in 0.001 secs (0.u,0.s) (successful) *) + +Goal True. + let x := smart_global:(id) in unfold x. + let x := smart_global:(aid) in unfold x. + let x := smart_global:(idn) in unfold x. +Abort. + +Goal id 0 = 0. + Opaque id. + assert_fails unfold_id. + Transparent id. + assert_succeeds unfold_id. + Opaque id. + Strategy 0 [id]. + assert_succeeds unfold_id. + Strategy 1 [id]. + assert_succeeds unfold_id. + Strategy -1 [id]. + assert_succeeds unfold_id. + Strategy opaque [id]. + assert_fails unfold_id. + Strategy transparent [id]. + assert_succeeds unfold_id. + Opaque id. + Strategy expand [id]. + assert_succeeds unfold_id. + reflexivity. +Qed. +Goal id 0 = 0. + Opaque aid. + assert_fails unfold_id. + Transparent aid. + assert_succeeds unfold_id. + Opaque aid. + Strategy 0 [aid]. + assert_succeeds unfold_id. + Strategy 1 [aid]. + assert_succeeds unfold_id. + Strategy -1 [aid]. + assert_succeeds unfold_id. + Strategy opaque [aid]. + assert_fails unfold_id. + Strategy transparent [aid]. + assert_succeeds unfold_id. + Opaque aid. + Strategy expand [aid]. + assert_succeeds unfold_id. + reflexivity. +Qed. +Goal id 0 = 0. + Opaque idn. + assert_fails unfold_id. + Transparent idn. + assert_succeeds unfold_id. + Opaque idn. + Strategy 0 [idn]. + assert_succeeds unfold_id. + Strategy 1 [idn]. + assert_succeeds unfold_id. + Strategy -1 [idn]. + assert_succeeds unfold_id. + Strategy opaque [idn]. + assert_fails unfold_id. + Strategy transparent [idn]. + assert_succeeds unfold_id. + Opaque idn. + Strategy expand [idn]. + assert_succeeds unfold_id. + reflexivity. +Qed. diff --git a/test-suite/success/with_strategy.v b/test-suite/success/with_strategy.v new file mode 100644 index 0000000000..bf639ae6b9 --- /dev/null +++ b/test-suite/success/with_strategy.v @@ -0,0 +1,527 @@ +Notation aid := (@id) (only parsing). +Notation idn := id (only parsing). +Ltac unfold_id := unfold id. + +Fixpoint fact (n : nat) + := match n with + | 0 => 1 + | S n => (S n) * fact n + end. + +Opaque id. +Goal id 0 = 0. + with_strategy + opaque [id] + (with_strategy + opaque [id id] + (assert_fails unfold_id; + with_strategy + transparent [id] + (assert_succeeds unfold_id; + with_strategy + opaque [id] + (with_strategy + 0 [id] + (assert_succeeds unfold_id; + with_strategy + 1 [id] + (assert_succeeds unfold_id; + with_strategy + -1 [id] + (assert_succeeds unfold_id; + with_strategy + opaque [id] + (assert_fails unfold_id; + with_strategy + transparent [id] + (assert_succeeds unfold_id; + with_strategy + opaque [id] + (with_strategy + expand [id] + (assert_succeeds unfold_id; + let l := strategy_level:(expand) in + with_strategy + l [id] + (let idx := smart_global:(id) in + cbv [idx]; + (* This should succeed, but doesn't, basically due to https://github.com/coq/coq/issues/11202 *) + assert_fails + (let idx := smart_global:(id) in + with_strategy + expand [idx] + idtac); + reflexivity)))))))))))). +Qed. +Goal id 0 = 0. + with_strategy + opaque [aid] + (assert_fails unfold_id; + with_strategy + transparent [aid] + (assert_succeeds unfold_id; + with_strategy + opaque [aid] + (with_strategy + 0 [aid] + (assert_succeeds unfold_id; + with_strategy + 1 [aid] + (assert_succeeds unfold_id; + with_strategy + -1 [aid] + (assert_succeeds unfold_id; + with_strategy + opaque [aid] + (assert_fails unfold_id; + with_strategy + transparent [aid] + (assert_succeeds unfold_id; + with_strategy + opaque [aid] + (with_strategy + expand [aid] + (assert_succeeds unfold_id; + reflexivity)))))))))). +Qed. +Goal id 0 = 0. + with_strategy + opaque [idn] + (assert_fails unfold_id; + with_strategy + transparent [idn] + (assert_succeeds unfold_id; + with_strategy + opaque [idn] + (with_strategy + 0 [idn] + (assert_succeeds unfold_id; + with_strategy + 1 [idn] + (assert_succeeds unfold_id; + with_strategy + -1 [idn] + (assert_succeeds unfold_id; + with_strategy + opaque [idn] + (assert_fails unfold_id; + with_strategy + transparent [idn] + (assert_succeeds unfold_id; + with_strategy + opaque [idn] + (with_strategy + expand [idn] + (assert_succeeds unfold_id; + reflexivity)))))))))). +Qed. + +(* test that strategy tactic does not persist after the execution of the tactic *) +Opaque id. +Goal id 0 = 0. + assert_fails unfold_id; + (with_strategy transparent [id] assert_succeeds unfold_id); + assert_fails unfold_id. + assert_fails unfold_id. + with_strategy transparent [id] assert_succeeds unfold_id. + assert_fails unfold_id. + reflexivity. +Qed. + +(* test that the strategy tactic does persist through abstract *) +Opaque id. +Goal id 0 = 0. + Fail Time Timeout 5 + with_strategy + expand [id] + assert (id (fact 100) = fact 100) by abstract reflexivity. + reflexivity. +Time Timeout 5 Defined. + +(* check that module substitutions happen correctly *) +Module F. + Definition id {T} := @id T. + Opaque id. + Ltac with_transparent_id tac := with_strategy transparent [id] tac. +End F. +Opaque F.id. + +Goal F.id 0 = F.id 0. + Fail unfold F.id. + (* This should work, but it fails with "Cannot coerce F.id to an evaluable reference." *) + Fail F.with_transparent_id ltac:(progress unfold F.id). + F.with_transparent_id ltac:(let x := constr:(@F.id) in progress unfold x). +Abort. + +Module Type Empty. End Empty. +Module E. End E. +Module F2F (E : Empty). + Definition id {T} := @id T. + Opaque id. + Ltac with_transparent_id tac := with_strategy transparent [id] tac. +End F2F. +Module F2 := F2F E. +Opaque F2.id. + +Goal F2.id 0 = F2.id 0. + Fail unfold F2.id. + (* This should work, but it fails with "Cannot coerce F2.id to an evaluable reference." *) + Fail F2.with_transparent_id ltac:(progress unfold F2.id). + F2.with_transparent_id ltac:(let x := constr:(@F2.id) in progress unfold x). +Abort. + +(* test the tactic notation entries *) +Tactic Notation "with_strategy0" strategy_level(l) "[" ne_smart_global_list(v) "]" tactic3(tac) := with_strategy l [ v ] tac. +Tactic Notation "with_strategy1" strategy_level_or_var(l) "[" ne_smart_global_list(v) "]" tactic3(tac) := with_strategy l [ v ] tac. +Tactic Notation "with_strategy2" strategy_level(l) "[" constr(v) "]" tactic3(tac) := with_strategy l [ v ] tac. +Tactic Notation "with_strategy3" strategy_level_or_var(l) "[" constr(v) "]" tactic3(tac) := with_strategy l [ v ] tac. + +(* [with_strategy0] should work, but it doesn't, due to a combination of https://github.com/coq/coq/issues/11202 and https://github.com/coq/coq/issues/11209 *) +Opaque id. +Goal id 0 = 0. + Fail (* should work, not Fail *) with_strategy0 opaque [id] idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [id id] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy0 transparent [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [id] idtac. + Fail (* should work, not Fail *) with_strategy0 0 [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 1 [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 -1 [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [id] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy0 transparent [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [id] idtac. + Fail (* should work, not Fail *) with_strategy0 expand [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + (* This should succeed, but doesn't, basically due to https://github.com/coq/coq/issues/11202 *) + Fail let idx := smart_global:(id) in + with_strategy0 expand [idx] idtac. + reflexivity. +Qed. +Goal id 0 = 0. + Fail (* should work, not Fail *) with_strategy0 opaque [aid] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy0 transparent [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [aid] idtac. + Fail (* should work, not Fail *) with_strategy0 0 [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 1 [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 -1 [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [aid] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy0 transparent [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [aid] idtac. + Fail (* should work, not Fail *) with_strategy0 expand [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + reflexivity. +Qed. +Goal id 0 = 0. + Fail (* should work, not Fail *) with_strategy0 opaque [idn] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy0 transparent [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [idn] idtac. + Fail (* should work, not Fail *) with_strategy0 0 [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 1 [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 -1 [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [idn] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy0 transparent [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [idn] idtac. + Fail (* should work, not Fail *) with_strategy0 expand [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + reflexivity. +Qed. + +(* [with_strategy1] should work, but it doesn't, due to a combination of https://github.com/coq/coq/issues/11202 and https://github.com/coq/coq/issues/11209 *) +Opaque id. +Goal id 0 = 0. + Fail (* should work, not Fail *) with_strategy1 opaque [id] idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [id id] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy1 transparent [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [id] idtac. + Fail (* should work, not Fail *) with_strategy1 0 [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 1 [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 -1 [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [id] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy1 transparent [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [id] idtac. + Fail (* should work, not Fail *) with_strategy1 expand [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) let l := strategy_level:(expand) in + with_strategy1 l [id] idtac. + (* This should succeed, but doesn't, basically due to https://github idtac.com/coq/coq/issues/11202 *) + Fail let idx := smart_global:(id) in + with_strategy1 expand [idx] idtac. + reflexivity. +Qed. +Goal id 0 = 0. + Fail (* should work, not Fail *) with_strategy1 opaque [aid] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy1 transparent [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [aid] idtac. + Fail (* should work, not Fail *) with_strategy1 0 [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 1 [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 -1 [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [aid] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy1 transparent [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [aid] idtac. + Fail (* should work, not Fail *) with_strategy1 expand [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + reflexivity. +Qed. +Goal id 0 = 0. + Fail (* should work, not Fail *) with_strategy1 opaque [idn] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy1 transparent [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [idn] idtac. + Fail (* should work, not Fail *) with_strategy1 0 [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 1 [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 -1 [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [idn] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy1 transparent [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [idn] idtac. + Fail (* should work, not Fail *) with_strategy1 expand [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + reflexivity. +Qed. + +Opaque id. +Goal id 0 = 0. + with_strategy2 + opaque [id] + (with_strategy2 + opaque [id] + (assert_fails unfold_id; + with_strategy2 + transparent [id] + (assert_succeeds unfold_id; + with_strategy2 + opaque [id] + (with_strategy2 + 0 [id] + (assert_succeeds unfold_id; + with_strategy2 + 1 [id] + (assert_succeeds unfold_id; + with_strategy2 + -1 [id] + (assert_succeeds unfold_id; + with_strategy2 + opaque [id] + (assert_fails unfold_id; + with_strategy2 + transparent [id] + (assert_succeeds unfold_id; + with_strategy2 + opaque [id] + (with_strategy2 + expand [id] + (assert_succeeds unfold_id))))))))))). + (* This should succeed, but doesn't, basically due to https://github.com/coq/coq/issues/11202 *) + Fail let idx := smart_global:(id) in + with_strategy2 expand [idx] idtac. + reflexivity. +Qed. +Goal id 0 = 0. + with_strategy2 + opaque [aid] + (with_strategy2 + opaque [aid] + (assert_fails unfold_id; + with_strategy2 + transparent [aid] + (assert_succeeds unfold_id; + with_strategy2 + opaque [aid] + (with_strategy2 + 0 [aid] + (assert_succeeds unfold_id; + with_strategy2 + 1 [aid] + (assert_succeeds unfold_id; + with_strategy2 + -1 [aid] + (assert_succeeds unfold_id; + with_strategy2 + opaque [aid] + (assert_fails unfold_id; + with_strategy2 + transparent [aid] + (assert_succeeds unfold_id; + with_strategy2 + opaque [aid] + (with_strategy2 + expand [aid] + (assert_succeeds unfold_id))))))))))). + reflexivity. +Qed. +Goal id 0 = 0. + with_strategy2 + opaque [idn] + (with_strategy2 + opaque [idn] + (assert_fails unfold_id; + with_strategy2 + transparent [idn] + (assert_succeeds unfold_id; + with_strategy2 + opaque [idn] + (with_strategy2 + 0 [idn] + (assert_succeeds unfold_id; + with_strategy2 + 1 [idn] + (assert_succeeds unfold_id; + with_strategy2 + -1 [idn] + (assert_succeeds unfold_id; + with_strategy2 + opaque [idn] + (assert_fails unfold_id; + with_strategy2 + transparent [idn] + (assert_succeeds unfold_id; + with_strategy2 + opaque [idn] + (with_strategy2 + expand [idn] + (assert_succeeds unfold_id))))))))))). + reflexivity. +Qed. + +Opaque id. +Goal id 0 = 0. + with_strategy3 + opaque [id] + (with_strategy3 + opaque [id] + (assert_fails unfold_id; + with_strategy3 + transparent [id] + (assert_succeeds unfold_id; + with_strategy3 + opaque [id] + (with_strategy3 + 0 [id] + (assert_succeeds unfold_id; + with_strategy3 + 1 [id] + (assert_succeeds unfold_id; + with_strategy3 + -1 [id] + (assert_succeeds unfold_id; + with_strategy3 + opaque [id] + (assert_fails unfold_id; + with_strategy3 + transparent [id] + (assert_succeeds unfold_id; + with_strategy3 + opaque [id] + (with_strategy3 + expand [id] + (assert_succeeds unfold_id))))))))))). + (* This should succeed, but doesn't, basically due to https://github.com/coq/coq/issues/11202 *) + Fail let idx := smart_global:(id) in + with_strategy3 expand [idx] idtac. + reflexivity. +Qed. +Goal id 0 = 0. + with_strategy3 + opaque [aid] + (with_strategy3 + opaque [aid] + (assert_fails unfold_id; + with_strategy3 + transparent [aid] + (assert_succeeds unfold_id; + with_strategy3 + opaque [aid] + (with_strategy3 + 0 [aid] + (assert_succeeds unfold_id; + with_strategy3 + 1 [aid] + (assert_succeeds unfold_id; + with_strategy3 + -1 [aid] + (assert_succeeds unfold_id; + with_strategy3 + opaque [aid] + (assert_fails unfold_id; + with_strategy3 + transparent [aid] + (assert_succeeds unfold_id; + with_strategy3 + opaque [aid] + (with_strategy3 + expand [aid] + (assert_succeeds unfold_id))))))))))). + reflexivity. +Qed. +Goal id 0 = 0. + with_strategy3 + opaque [idn] + (with_strategy3 + opaque [idn] + (assert_fails unfold_id; + with_strategy3 + transparent [idn] + (assert_succeeds unfold_id; + with_strategy3 + opaque [idn] + (with_strategy3 + 0 [idn] + (assert_succeeds unfold_id; + with_strategy3 + 1 [idn] + (assert_succeeds unfold_id; + with_strategy3 + -1 [idn] + (assert_succeeds unfold_id; + with_strategy3 + opaque [idn] + (assert_fails unfold_id; + with_strategy3 + transparent [idn] + (assert_succeeds unfold_id; + with_strategy3 + opaque [idn] + (with_strategy3 + expand [idn] + (assert_succeeds unfold_id))))))))))). + reflexivity. +Qed. diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 3cb10364b5..049c3a0844 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -790,12 +790,6 @@ GRAMMAR EXTEND Gram { List.map (fun name -> (name.CAst.v, MaxImplicit)) items } ] ]; - strategy_level: - [ [ IDENT "expand" -> { Conv_oracle.Expand } - | IDENT "opaque" -> { Conv_oracle.Opaque } - | n=integer -> { Conv_oracle.Level n } - | IDENT "transparent" -> { Conv_oracle.transparent } ] ] - ; instance_name: [ [ name = ident_decl; bl = binders -> { (CAst.map (fun id -> Name id) (fst name), snd name), bl } |