diff options
| -rw-r--r-- | ide/ide_slave.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index a4e84903e..1000101a4 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -124,7 +124,7 @@ let annotate phrase = Vernac.parse_sentence (pa,None) in let (_, _, xml) = - RichPrinter.richpp_vernac ast + Richprinter.richpp_vernac ast in xml |