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 /user-contrib | |
| parent | 751afe3f52e52f14cf0972498d84722519dd91e7 (diff) | |
turn Ltac2's `pattern:` into `pat:`
Diffstat (limited to 'user-contrib')
| -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 |
3 files changed, 3 insertions, 3 deletions
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 -> |