diff options
| author | Théo Zimmermann | 2019-06-19 10:41:09 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-06-19 10:41:09 +0200 |
| commit | cdba5f7ceee1adfbdd96ffc82115fbc1e6750b80 (patch) | |
| tree | e4e94c235b18bdf96b82db071da74535ccd827c5 /plugins/ltac/extraargs.mlg | |
| parent | 415e83efb9e767ddf65b8c27d4e497592fd61f2c (diff) | |
| parent | 459b5ce5b2b825db43d645357f83d7fe17289bc5 (diff) | |
Merge PR #10239: Deprecate grammar entry "intropattern" in tactic notations in favor of "simple_intropattern"
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
Diffstat (limited to 'plugins/ltac/extraargs.mlg')
| -rw-r--r-- | plugins/ltac/extraargs.mlg | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index 5a7ce4c3da..2654729652 100644 --- a/plugins/ltac/extraargs.mlg +++ b/plugins/ltac/extraargs.mlg @@ -35,7 +35,7 @@ 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 let () = create_generic_quotation "constr" Pcoq.Constr.lconstr Stdarg.wit_constr -let () = create_generic_quotation "ipattern" Pltac.simple_intropattern wit_intro_pattern +let () = create_generic_quotation "ipattern" Pltac.simple_intropattern wit_simple_intropattern let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Stdarg.wit_open_constr let () = let inject (loc, v) = Tacexpr.Tacexp v in @@ -46,7 +46,7 @@ let () = let () = let register name entry = Tacentries.register_tactic_notation_entry name entry in register "hyp" wit_var; - register "simple_intropattern" wit_intro_pattern; + register "simple_intropattern" wit_simple_intropattern; register "integer" wit_integer; register "reference" wit_ref; () |