diff options
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 2b6684448..e19be4e12 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -960,7 +960,7 @@ and pr_extend s cl = try pr_gen a with Failure _ -> str ("<error in "^s^">") in try - let rls = List.assoc s (Egramml.get_extend_vernac_grammars()) in + let rls = List.assoc_f String.equal s (Egramml.get_extend_vernac_grammars()) in let rl = match_vernac_rule (List.map Genarg.genarg_tag cl) rls in let start,rl,cl = match rl with |