diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 1 | ||||
| -rw-r--r-- | dev/top_printers.ml | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/dev/base_include b/dev/base_include index 83e23d29f5..d3301c88bd 100644 --- a/dev/base_include +++ b/dev/base_include @@ -72,6 +72,7 @@ open Classops open Clenv open Rawterm open Coercion +open Coercion.Default open Recordops open Detyping open Reductionops diff --git a/dev/top_printers.ml b/dev/top_printers.ml index dfd8139855..c67307d36f 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -48,6 +48,7 @@ let ppcon con = pp(pr_con con) let ppkn kn = pp(pr_kn kn) let ppsp sp = pp(pr_sp sp) let ppqualid qid = pp(pr_qualid qid) +let ppclindex cl = pp(Classops.pr_cl_index cl) (* term printers *) let rawdebug = ref false |