Commit 9521a499 authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

[Coq] From dom/assoc to a ternary Position relation

parent 3c913f52
This diff is collapsed.
......@@ -121,7 +121,7 @@ let rec print_term out_fmter : tterm -> unit = function
print_label l
print_meth m
| Tcast (t, ty1, ty2) ->
Format.fprintf out_fmter "@[<hov>Expr_coerce@ %a@ %a@ (subtype_dec_correct@ %a@ %a@ Istrue_true)@]"
Format.fprintf out_fmter "@[<hov>Expr_coerce@ %a@ %a@ (subtype_dec_correct@ %a@ %a@ I)@]"
print_par_ty ty2
print_par_term t
print_par_ty ty1
......@@ -132,17 +132,17 @@ and print_par_term out_fmter = function
Format.fprintf out_fmter "(%a)"
print_term t
and print_obj_elem out_fmter (l, m) =
Format.fprintf out_fmter "(@[<hov>%a =@ %a@])%%meth"
Format.fprintf out_fmter "@[<hov>%a @ %a@]"
print_label l
print_meth m
and print_obj_elems ty out_fmter = function
| [] ->
Format.fprintf out_fmter "(init@ %a@ Istrue_true)"
Format.fprintf out_fmter "(init@ %a)"
print_par_ty ty
| el :: els ->
Format.fprintf out_fmter "(pocons_3@ %a@ %a)"
print_obj_elem el
Format.fprintf out_fmter "(%a ## %a)"
(print_obj_elems ty) els
print_obj_elem el
and print_meth out_fmter (Tmeth (x, ty, body, _)) =
Format.fprintf out_fmter "@[<h>ς(%a !: %a)%a@]"
print_id x
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment