Commit c22da22d authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Only add an initial '_' to identifiers printed to Coq when they start by

a digit.
parent acf0eedf
......@@ -2,7 +2,17 @@ open Parsetree
open Scoper
open Typer
let print_id out_fmter (Id i) = Format.fprintf out_fmter "_%s" i
let print_id out_fmter (Id i) =
let s =
if i == ""
then "_"
else (
if i.[0] >= '0' && i.[0] <= '9' (* identifier starts with a digit, add an underscore in front *)
then "_" ^ i
else i)
in
Format.fprintf out_fmter "%s" s
let print_cid out_fmter (Cid c) = Format.fprintf out_fmter "%s" c
let print_label out_fmter (Label l) = Format.fprintf out_fmter "\"%s\"" l
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment