From 18859319b1daee0abb32bbc4e89ec5865a6fe082 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Mon, 1 Jun 2020 11:05:15 +0200
Subject: clightgen -short-idents : do not use $"xxx" notation ever

In the original code, collisions could occur: an identifier could
be numbered with a number that happens to be equal to its canonical
encoding.  This was harmless but confusing.

Closes: #358
---
 exportclight/ExportClight.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'exportclight')

diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index 87956b58..96947545 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -81,7 +81,7 @@ let define_idents p =
     string_of_atom
     (fun (id, name) ->
       try
-        if id = pos_of_string name then
+        if !use_canonical_atoms && id = pos_of_string name then
           fprintf p "Definition _%s : ident := $\"%s\".@ "
                     (sanitize name) name
         else
-- 
cgit