diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/printers.mllib | 3 | ||||
| -rw-r--r-- | dev/top_printers.ml | 2 |
2 files changed, 3 insertions, 2 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index 0b6ec899e9..7db5b5cb99 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -47,7 +47,8 @@ Cbytecodes Copcodes Cemitcodes Nativevalues -Declarations +Lazyconstr +Declareops Retroknowledge Pre_env Nativelambda diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 0dc09f9baf..db895fc0f7 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -49,7 +49,7 @@ let rawdebug = ref false let ppconstr x = pp (Termops.print_constr x) let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr x) let ppterm = ppconstr -let ppsconstr x = ppconstr (Declarations.force x) +let ppsconstr x = ppconstr (Lazyconstr.force x) let ppconstr_univ x = Constrextern.with_universes ppconstr x let ppglob_constr = (fun x -> pp(pr_lglob_constr x)) let pppattern = (fun x -> pp(pr_constr_pattern x)) |