Commit 1a10a4c7 authored by MARCHE Claude's avatar MARCHE Claude Committed by Guillaume Melquiond
Browse files

regression test for issue #43

parent 8e95f4ce
module Issue43
type t = < range 0 1 >
constant c : int = t'minInt
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
<why3session shape_version="4">
<file name="../43_range_module.mlw" proved="true">
<theory name="Issue43" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
Supports Markdown
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