summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorBrian Campbell2018-09-24 17:33:20 +0100
committerBrian Campbell2018-09-24 17:33:34 +0100
commit57380afc09bf5ce5748d2e21584474827c7eb76b (patch)
treec47743399d3ed7d2f19ba3d8d68b41265e2855e8 /src
parent738ea556ab030fad03577907ff46f2ba1a54dcb3 (diff)
Coq: avoid variables called tt (the unit constant)
Diffstat (limited to 'src')
-rw-r--r--src/pretty_print_coq.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 1ae31934..b4fc4a72 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -133,6 +133,7 @@ let rec fix_id remove_tick name = match name with
| "S"
| "mod"
| "M"
+ | "tt"
-> name ^ "'"
| _ ->
if String.contains name '#' then