diff options
Diffstat (limited to 'ide/ide_slave.ml')
| -rw-r--r-- | ide/ide_slave.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 88b61042ed..c77232ad15 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -111,8 +111,9 @@ let annotate phrase = let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in Vernac.parse_sentence (pa,None) in - Richpp.repr (Richpp.richpp_of_pp (Ppvernac.pr_vernac ast)) - + (* XXX: Width should be a parameter of annotate... *) + Richpp.richpp_of_pp (Ppvernac.pr_vernac ast) + (** Goal display *) let hyp_next_tac sigma env decl = |