diff options
| author | Pierre-Marie Pédrot | 2021-01-18 13:02:37 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-18 13:02:37 +0100 |
| commit | 5b08cdcd4bde7fdcd21f7a0f0912f0021847294b (patch) | |
| tree | f5358388ee4eee0a7b49f9b0de505940cdc33f46 /user-contrib | |
| parent | 3efb7a44dee255cd8f6cbd8c80e3c48c601104ed (diff) | |
| parent | 2a5e88b967f648887219e80aaf694395f1f15c1c (diff) | |
Merge PR #13574: Simplistic patch to fix #10113: turn Ltac2's `pattern:` into `pat:`
Ack-by: Zimmi48
Reviewed-by: jfehrle
Reviewed-by: ppedrot
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 64a2b24404..241ca7ad66 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -1151,7 +1151,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 -> |