diff options
Diffstat (limited to 'tactics/g_ltac.ml4')
| -rw-r--r-- | tactics/g_ltac.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/g_ltac.ml4 b/tactics/g_ltac.ml4 index 5c0ae215d..d75073877 100644 --- a/tactics/g_ltac.ml4 +++ b/tactics/g_ltac.ml4 @@ -401,7 +401,7 @@ VERNAC COMMAND EXTEND VernacTacticNotation CLASSIFIED AS SIDEFF [ let l = Locality.LocalityFixme.consume () in let n = Option.default 0 n in - Metasyntax.add_tactic_notation (Locality.make_module_locality l, n, r, e) + Tacentries.add_tactic_notation (Locality.make_module_locality l, n, r, e) ] END |