diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /dev/vm_printers.ml | |
parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) |
Imported Upstream version 8.9.0upstream/8.9.0upstream
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" |