Commit 992e36f2 authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

[FIX] coq_printer.ml missed the renaming Ecoerce -> Expr_coerce

parent 0f8af4e4
......@@ -121,9 +121,8 @@ let rec print_term out_fmter : tterm -> unit = function
print_label l
print_meth m
| Tcast (t, ty1, ty2) ->
Format.fprintf out_fmter "@[<hov>Ecoerce@ %a@ %a@ %a@ (subtype_dec_correct@ %a@ %a@ Istrue_true)@]"
Format.fprintf out_fmter "@[<hov>Expr_coerce@ %a@ %a@ (subtype_dec_correct@ %a@ %a@ Istrue_true)@]"
print_par_ty ty2
print_par_ty ty1
print_par_term t
print_par_ty ty1
print_par_ty ty2
......
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