diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/extraargs.ml4 | 7 | ||||
| -rw-r--r-- | plugins/ltac/plugin_base.dune | 13 | ||||
| -rw-r--r-- | plugins/ltac/tacenv.ml | 2 |
3 files changed, 19 insertions, 3 deletions
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index dbbdbfa396..d779951180 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -52,8 +52,11 @@ let () = (* Rewriting orientation *) -let _ = Metasyntax.add_token_obj "<-" -let _ = Metasyntax.add_token_obj "->" +let _ = + Mltop.declare_cache_obj + (fun () -> Metasyntax.add_token_obj "<-"; + Metasyntax.add_token_obj "->") + "ltac_plugin" let pr_orient _prc _prlc _prt = function | true -> Pp.mt () diff --git a/plugins/ltac/plugin_base.dune b/plugins/ltac/plugin_base.dune new file mode 100644 index 0000000000..5611f5ba16 --- /dev/null +++ b/plugins/ltac/plugin_base.dune @@ -0,0 +1,13 @@ +(library + (name ltac_plugin) + (public_name coq.plugins.ltac) + (synopsis "Coq's LTAC tactic language") + (modules :standard \ tauto) + (libraries coq.stm)) + +(library + (name tauto_plugin) + (public_name coq.plugins.tauto) + (synopsis "Coq's tauto tactic") + (modules tauto) + (libraries coq.plugins.ltac)) diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index 0bb9ccb1d8..1f2c722b34 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -144,7 +144,7 @@ let add ~deprecation kn b t = mactab := KNmap.add kn entry !mactab let replace kn path t = - let (path, _, _) = KerName.repr path in + let path = KerName.modpath path in let entry _ e = { e with tac_body = t; tac_redef = path :: e.tac_redef } in mactab := KNmap.modify kn entry !mactab |