13853b.mlw 271 Bytes
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16

(*

BTS 13853 (follow-up)

https://gforge.inria.fr/tracker/?func=detail&atid=10293&aid=13853&group_id=2990

*)


module T

  type t

  exception MyExc

17 18
  let rec f (x:t) : t raises { MyExc } = raise MyExc
  with g  (x:t) : t raises { MyExc } ensures { true } = f x
MARCHE Claude's avatar
MARCHE Claude committed
19 20
end