diff options
| -rw-r--r-- | doc/sphinx/changes.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 10 | ||||
| -rw-r--r-- | plugins/ssr/ssrparser.mlg | 75 |
3 files changed, 52 insertions, 37 deletions
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index fd84868a1f..6ac55e7bf4 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -102,10 +102,10 @@ reference manual. Here are the most important user-visible changes: extensionality lemma: - interactive mode: :n:`under @term`, associated terminator: :tacn:`over` - - one-liner mode: `under @term do [@tactic | ...]` + - one-liner mode: :n:`under @term do [@tactic | ...]` It can take occurrence switches, contextual patterns, and intro patterns: - :g:`under {2}[in RHS]eq_big => [i|i ?] do ...` + :g:`under {2}[in RHS]eq_big => [i|i ?]` (`#9651 <https://github.com/coq/coq/pull/9651>`_, by Erik Martin-Dorel and Enrico Tassi). diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 1b9e3ce0f3..ed980bd4de 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -3761,10 +3761,10 @@ involves the following steps: 5. If so :tacn:`under` protects these n goals against an accidental instantiation of the evar. - These protected goals are displayed using the ``Under[ … ]`` - notation (e.g. ``Under[ m - m ]`` in the running example). + These protected goals are displayed using the ``'Under[ … ]`` + notation (e.g. ``'Under[ m - m ]`` in the running example). -6. The expression inside the ``Under[ … ]`` notation can be +6. The expression inside the ``'Under[ … ]`` notation can be proved equivalent to the desired expression by using a regular :tacn:`rewrite` tactic. @@ -3782,7 +3782,7 @@ The over tactic Two equivalent facilities (a terminator and a lemma) are provided to close intermediate subgoals generated by :tacn:`under` (i.e. goals -displayed as ``Under[ … ]``): +displayed as ``'Under[ … ]``): .. tacn:: over :name: over @@ -3792,7 +3792,7 @@ displayed as ``Under[ … ]``): .. tacv:: by rewrite over - This is a variant of :tacn:`over` in order to close ``Under[ … ]`` + This is a variant of :tacn:`over` in order to close ``'Under[ … ]`` goals, relying on the ``over`` rewrite rule. .. _under_one_liner: diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 858a75698a..c09250ade5 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -68,6 +68,25 @@ DECLARE PLUGIN "ssreflect_plugin" { +let ssrtac_name name = { + mltac_plugin = "ssreflect_plugin"; + mltac_tactic = "ssr" ^ name; +} + +let ssrtac_entry name = { + mltac_name = ssrtac_name name; + mltac_index = 0; +} + +let register_ssrtac name f = + Tacenv.register_ml_tactic (ssrtac_name name) [|f|] + +let cast_arg wit v = Taccoerce.Value.cast (Genarg.topwit wit) v + +} + +{ + (* Defining grammar rules with "xx" in it automatically declares keywords too, * we thus save the lexer to restore it at the end of the file *) let frozen_lexer = CLexer.get_keyword_state () ;; @@ -969,14 +988,17 @@ ARGUMENT EXTEND ssrintrosarg TYPED AS (tactic * ssrintros) | [ "YouShouldNotTypeThis" ssrtacarg(arg) ssrintros_ne(ipats) ] -> { arg, ipats } END -TACTIC EXTEND ssrtclintros -| [ "YouShouldNotTypeThis" ssrintrosarg(arg) ] -> - { let tac, intros = arg in - ssrevaltac ist tac <*> tclIPATssr intros } -END - { +let () = register_ssrtac "tclintros" begin fun args ist -> match args with +| [arg] -> + let arg = cast_arg wit_ssrintrosarg arg in + let tac, intros = arg in + ssrevaltac ist tac <*> tclIPATssr intros +| _ -> assert false +end + + (** Defined identifier *) let pr_ssrfwdid id = pr_spc () ++ pr_id id @@ -1701,16 +1723,6 @@ let _ = add_internal_name (is_tagged perm_tag) type ssrargfmt = ArgSsr of string | ArgSep of string -let ssrtac_name name = { - mltac_plugin = "ssreflect_plugin"; - mltac_tactic = "ssr" ^ name; -} - -let ssrtac_entry name n = { - mltac_name = ssrtac_name name; - mltac_index = n; -} - let set_pr_ssrtac name prec afmt = (* FIXME *) () (* let fmt = List.map (function | ArgSep s -> Egramml.GramTerminal s @@ -1718,8 +1730,7 @@ let set_pr_ssrtac name prec afmt = (* FIXME *) () (* | ArgCoq at -> Egramml.GramTerminal "COQ_ARG") afmt in let tacname = ssrtac_name name in () *) -let ssrtac_atom ?loc name args = TacML (CAst.make ?loc (ssrtac_entry name 0, args)) -let ssrtac_expr ?loc name args = ssrtac_atom ?loc name args +let ssrtac_expr ?loc name args = TacML (CAst.make ?loc (ssrtac_entry name, args)) let tclintros_expr ?loc tac ipats = let args = [Tacexpr.TacGeneric (in_gen (rawwit wit_ssrintrosarg) (tac, ipats))] in @@ -1802,15 +1813,15 @@ END (** The "do" tactical. ********************************************************) -(* -type ssrdoarg = ((ssrindex * ssrmmod) * ssrhint) * ssrclauses -*) -TACTIC EXTEND ssrtcldo -| [ "YouShouldNotTypeThis" "do" ssrdoarg(arg) ] -> { V82.tactic (ssrdotac ist arg) } -END - { +let () = register_ssrtac "tcldo" begin fun args ist -> match args with +| [arg] -> + let arg = cast_arg wit_ssrdoarg arg in + V82.tactic (ssrdotac ist arg) +| _ -> assert false +end + let _ = set_pr_ssrtac "tcldo" 3 [ArgSep "do "; ArgSsr "doarg"] let ssrdotac_expr ?loc n m tac clauses = @@ -1849,13 +1860,17 @@ let pr_ssrseqdir _ _ _ = function ARGUMENT EXTEND ssrseqdir TYPED AS ssrdir PRINTED BY { pr_ssrseqdir } END -TACTIC EXTEND ssrtclseq -| [ "YouShouldNotTypeThis" ssrtclarg(tac) ssrseqdir(dir) ssrseqarg(arg) ] -> - { V82.tactic (tclSEQAT ist tac dir arg) } -END - { +let () = register_ssrtac "tclseq" begin fun args ist -> match args with +| [tac; dir; arg] -> + let tac = cast_arg wit_ssrtclarg tac in + let dir = cast_arg wit_ssrseqdir dir in + let arg = cast_arg wit_ssrseqarg arg in + V82.tactic (tclSEQAT ist tac dir arg) +| _ -> assert false +end + let _ = set_pr_ssrtac "tclseq" 5 [ArgSsr "tclarg"; ArgSsr "seqdir"; ArgSsr "seqarg"] let tclseq_expr ?loc tac dir arg = |