Commit 9ed7c6bc authored by Sylvain Dailler's avatar Sylvain Dailler

Add test for #138

Corrected typo in Pretty.ml
parent 3e802ac9
module Test
use int.Int
type a = < range 22 46 >
let f (b : a) =
requires {a'int b = 42}
ensures {a'int result = a'int b}
(42:a)
end
module Test2
use int.Int
let f (b : int) =
requires {b = 42}
ensures {result = b}
42
end
module Test1
clone Test2 as T (* Replace with Test does not work *)
end
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<file name="../138.mlw">
<theory name="Test">
<goal name="VC f" expl="VC for f">
</goal>
</theory>
<theory name="Test2">
<goal name="VC f" expl="VC for f">
</goal>
</theory>
</file>
</why3session>
......@@ -403,7 +403,7 @@ let print_ty_decl fmt ts =
| NoDef -> ()
| Alias ty -> fprintf fmt " =@ %a" print_ty ty
| Range ir ->
fprintf fmt " =@ <range %s .. %s>"
fprintf fmt " =@ <range %s %s>"
(BigInt.to_string ir.Number.ir_lower)
(BigInt.to_string ir.Number.ir_upper)
| Float irf ->
......
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