diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/top_printers.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index cd0fa0c0d6..27577c79cf 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -48,7 +48,7 @@ let ppqualid qid = pp(pr_qualid qid) (* term printers *) let ppconstr x = pp (Termops.print_constr x) -let ppconstrdb x = pp(Options.with_option Constrextern.rawdebug Termops.print_constr x) +let ppconstrdb x = pp(Flags.with_option Constrextern.rawdebug Termops.print_constr x) let ppterm = ppconstr let ppsconstr x = ppconstr (Declarations.force x) let ppconstr_univ x = Constrextern.with_universes ppconstr x |