summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/pretty_print_coq.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 52ecc715..aaef83cb 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -135,6 +135,8 @@ let rec fix_id remove_tick name = match name with
| "GT"
| "EQ"
| "Z"
+ | "O"
+ | "S"
| "mod"
| "M"
-> name ^ "'"