Commit dc81b215 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Avoid parenthesizing simple real numbers in Coq.

I am assuming these numbers are not negative. This assumption has always
existed for integers and the lexer cannot create negative real numbers
anyway. So, as long as a transformation does not create negative numbers,
there won't be any issue. (Transformations applying a negation to positive
numbers are fine though.)
parent d7f20f9c
......@@ -221,7 +221,7 @@ and print_tnode opl opr info fmt t = match t.t_node with
Print_number.dec_real_support = Print_number.Number_unsupported;
Print_number.hex_real_support = Print_number.Number_unsupported;
Print_number.frac_real_support = Print_number.Number_custom
(Print_number.PrintFracReal ("(%s)%%R", "(%s * %s)%%R", "(%s / %s)%%R"));
(Print_number.PrintFracReal ("%s%%R", "(%s * %s)%%R", "(%s / %s)%%R"));
Print_number.def_real_support = Print_number.Number_unsupported;
} in
Print_number.print number_format fmt c
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment