summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorBrian Campbell2018-07-06 17:36:33 +0100
committerBrian Campbell2018-07-06 18:27:01 +0100
commita41ca0c0ed6acdb17362886c4c9650c4c353afef (patch)
tree633a0a64867bb4cba9c269d2cfa1698d549912dd /src
parentf1f3c68878406ae5029881e20b839d2b6f535280 (diff)
Coq: Avoid clashes with the monad name, M
Diffstat (limited to 'src')
-rw-r--r--src/pretty_print_coq.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 9cc85601..1eb62193 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -136,6 +136,7 @@ let rec fix_id remove_tick name = match name with
| "EQ"
| "Z"
| "mod"
+ | "M"
-> name ^ "'"
| _ ->
if String.contains name '#' then
@@ -146,7 +147,7 @@ let rec fix_id remove_tick name = match name with
fix_id remove_tick (String.concat "__" (Util.split_on_char '^' name))
else if name.[0] = '\'' then
let var = String.sub name 1 (String.length name - 1) in
- if remove_tick then var else (var ^ "'")
+ if remove_tick then fix_id remove_tick var else (var ^ "'")
else if is_number_char(name.[0]) then
("v" ^ name ^ "'")
else name