'distinct' is a keyword for Alt-Ergo

42a1adb2 · Jean-Christophe Filliâtre · 5dadfbe2 · 42a1adb2
Commit 42a1adb2 authored Aug 05, 2011 by Jean-Christophe Filliâtre
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 1 deletion

src/printer/alt_ergo.ml src/printer/alt_ergo.ml +1 -1

No files found.
--- a/src/printer/alt_ergo.ml
+++ b/src/printer/alt_ergo.ml
@@ -32,7 +32,7 @@ let meta_ac = Theory.register_meta "AC" [Theory.MTlsymbol]

 let ident_printer =
  let bls = [
-    "ac"; "and"; "array"; "as"; "axiom"; "bool"; "else"; "exists";
+    "ac"; "and"; "array"; "as"; "axiom"; "bool"; "distinct"; "else"; "exists";
    "false"; "forall"; "function"; "goal"; "if"; "int"; "bitv";
    "logic"; "not"; "or"; "parameter"; "predicate";
    "prop"; "real"; "then"; "true"; "type"; "unit"; "void";