diff options
Diffstat (limited to 'vernac/g_proofs.mlg')
| -rw-r--r-- | vernac/g_proofs.mlg | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index cccdbfc91..dacef6e21 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -22,7 +22,7 @@ open Pvernac.Vernac_ let thm_token = G_vernac.thm_token -let hint = Gram.entry_create "hint" +let hint = Entry.create "hint" let warn_deprecated_focus = CWarnings.create ~name:"deprecated-focus" ~category:"deprecated" |