diff options
| author | Kenji Maillard | 2020-12-04 20:38:16 +0100 |
|---|---|---|
| committer | Kenji Maillard | 2020-12-04 20:41:24 +0100 |
| commit | 723d695e86cc74ab11edb97acdfced0566be7131 (patch) | |
| tree | bf097517bd4b7afba5da7fc6dafc6a8b810fe2b5 | |
| parent | 751afe3f52e52f14cf0972498d84722519dd91e7 (diff) | |
turn Ltac2's `pattern:` into `pat:`
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 4 | ||||
| -rw-r--r-- | user-contrib/Ltac2/g_ltac2.mlg | 2 | ||||
| -rw-r--r-- | user-contrib/Ltac2/tac2core.ml | 2 | ||||
| -rw-r--r-- | user-contrib/Ltac2/tac2print.ml | 2 |
4 files changed, 5 insertions, 5 deletions
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 375129c02d..286eaa1a4d 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -557,7 +557,7 @@ Built-in quotations ltac2_quotations ::= ident : ( @lident ) | constr : ( @term ) | open_constr : ( @term ) - | pattern : ( @cpattern ) + | pat : ( @cpattern ) | reference : ( {| & @ident | @qualid } ) | ltac1 : ( @ltac1_expr_in_env ) | ltac1val : ( @ltac1_expr_in_env ) @@ -571,7 +571,7 @@ The current implementation recognizes the following built-in quotations: (type ``Init.constr``). - ``open_constr``, which parses Coq terms and produces a term potentially with holes at runtime (type ``Init.constr`` as well). -- ``pattern``, which parses Coq patterns and produces a pattern used for term +- ``pat``, which parses Coq patterns and produces a pattern used for term matching (type ``Init.pattern``). - ``reference`` Qualified names are globalized at internalization into the corresponding global reference, diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index 65b61a0d93..548e12d611 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -213,7 +213,7 @@ GRAMMAR EXTEND Gram | IDENT "constr"; ":"; "("; c = Constr.lconstr; ")" -> { Tac2quote.of_constr c } | IDENT "open_constr"; ":"; "("; c = Constr.lconstr; ")" -> { Tac2quote.of_open_constr c } | IDENT "ident"; ":"; "("; c = lident; ")" -> { Tac2quote.of_ident c } - | IDENT "pattern"; ":"; "("; c = Constr.cpattern; ")" -> { inj_pattern loc c } + | IDENT "pat"; ":"; "("; c = Constr.cpattern; ")" -> { inj_pattern loc c } | IDENT "reference"; ":"; "("; c = globref; ")" -> { inj_reference loc c } | IDENT "ltac1"; ":"; "("; qid = ltac1_expr_in_env; ")" -> { inj_ltac1 loc qid } | IDENT "ltac1val"; ":"; "("; qid = ltac1_expr_in_env; ")" -> { inj_ltac1val loc qid } diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index 8663691c0a..82e5c34842 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -1147,7 +1147,7 @@ let () = let sigma = Evd.from_env env in Patternops.subst_pattern env sigma subst c in - let print env sigma pat = str "pattern:(" ++ Printer.pr_lconstr_pattern_env env sigma pat ++ str ")" in + let print env sigma pat = str "pat:(" ++ Printer.pr_lconstr_pattern_env env sigma pat ++ str ")" in let interp _ c = return (Value.of_pattern c) in let obj = { ml_intern = intern; diff --git a/user-contrib/Ltac2/tac2print.ml b/user-contrib/Ltac2/tac2print.ml index fe62de1fb3..a54eb45f61 100644 --- a/user-contrib/Ltac2/tac2print.ml +++ b/user-contrib/Ltac2/tac2print.ml @@ -466,7 +466,7 @@ end let () = register_init "pattern" begin fun env sigma c -> let c = to_pattern c in let c = try Printer.pr_lconstr_pattern_env env sigma c with _ -> str "..." in - str "pattern:(" ++ c ++ str ")" + str "pat:(" ++ c ++ str ")" end let () = register_init "message" begin fun _ _ pp -> |