Merge branch 'fix_proofs_with_coq_8_19' into 'master'

[why3.git] / drivers / pvs-realize.drv

(*
prelude "% This file is generated by Why3's PVS driver"
prelude "% Beware! Only edit allowed sections below   "
*)

printer "pvs-realize"
filename "%t.pvs"

import "pvs-common.gen"