diff options
Diffstat (limited to 'dev/vm_printers.ml')
| -rw-r--r-- | dev/vm_printers.ml | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index 2ddf927d..ea126e27 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -1,7 +1,7 @@ open Format open Term +open Constr open Names -open Cbytecodes open Cemitcodes open Vmvalues @@ -10,11 +10,14 @@ let ppripos (ri,pos) = | Reloc_annot a -> let sp,i = a.ci.ci_ind in print_string - ("annot : MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^")\n") + ("annot : MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^")\n") | Reloc_const _ -> print_string "structured constant\n" | Reloc_getglobal kn -> - print_string ("getglob "^(Constant.to_string kn)^"\n")); + print_string ("getglob "^(Constant.to_string kn)^"\n") + | Reloc_proj_name p -> + print_string ("proj "^(Projection.Repr.to_string p)^"\n") + ); print_flush () let print_vfix () = print_string "vfix" @@ -22,8 +25,8 @@ let print_vfix_app () = print_string "vfix_app" let print_vswith () = print_string "switch" let ppsort = function - | Prop(Pos) -> print_string "Set" - | Prop(Null) -> print_string "Prop" + | Set -> print_string "Set" + | Prop -> print_string "Prop" | Type u -> print_string "Type" |