Commit a200be98 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix missing space when outputting negated inequalities for Gappa.

parent eba91a64
......@@ -44,8 +44,8 @@ theory int.Int
meta "gappa arith" logic (<=), "", "<=", ">="
meta "gappa arith" logic (>=), "", ">=", "<="
meta "gappa arith" logic (<), "not", ">=", "<="
meta "gappa arith" logic (>), "not", "<=", ">="
meta "gappa arith" logic (<), "not ", ">=", "<="
meta "gappa arith" logic (>), "not ", "<=", ">="
meta "inline : no" logic (<=)
meta "inline : no" logic (>=)
......@@ -100,8 +100,8 @@ theory real.Real
meta "gappa arith" logic (<=), "", "<=", ">="
meta "gappa arith" logic (>=), "", ">=", "<="
meta "gappa arith" logic (<), "not", ">=", "<="
meta "gappa arith" logic (>), "not", "<=", ">="
meta "gappa arith" logic (<), "not ", ">=", "<="
meta "gappa arith" logic (>), "not ", "<=", ">="
meta "inline : no" logic (<=)
meta "inline : no" logic (>=)
......
......@@ -41,7 +41,7 @@ type info = {
let int_minus = ref ps_equ
let real_minus = ref ps_equ
(** lsymbol, ""/"not", op, rev_op *)
(** lsymbol, ""/"not ", op, rev_op *)
let arith_meta = register_meta "gappa arith"
[MTlsymbol;MTstring;MTstring;MTstring]
......
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