Skip to content

why3
why3
Commit 378da39d authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files
Options

Restore short type names for int and real in the Coq driver.

parent 726b3f5b
Hide whitespace changes
Inline Side-by-side
Showing with 2 additions and 0 deletions
drivers/coq-common.gen
View file @ 378da39d
......@@ -23,6 +23,8 @@ theory BuiltIn
prelude "Require Import BuiltIn."
syntax type int "Z"
syntax type real "R"
syntax predicate (=) "(%1 = %2)"
end
......
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