diff options
| author | Pierre Letouzey | 2018-04-06 14:38:02 +0200 |
|---|---|---|
| committer | Jason Gross | 2018-08-31 20:05:52 -0400 |
| commit | 5df8f2ed3d9cf8d7903568308d8ce2e8e6dd4720 (patch) | |
| tree | 213558e5b207b40a4b7ef11db452402bd6ccf33e /plugins | |
| parent | 3099be05553dab10b41d864f4981860eb105f145 (diff) | |
Tacenv: minor code cleanup
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/tacenv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |