From ed36d0e0d7b1e3859173f1148dfac3e90b7f3308 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sun, 29 Dec 2024 16:19:30 +0100 Subject: [PATCH] only output plain comments in generated Coq code --- src/defns.ml | 2 +- src/grammar_pp.ml | 6 ++---- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/src/defns.ml b/src/defns.ml index 8eed307..90727f6 100644 --- a/src/defns.ml +++ b/src/defns.ml @@ -953,7 +953,7 @@ let pp_fun_or_reln_defnclass_list List.iter (fun frdc -> pp_fun_or_reln_defnclass fd m xd lookup frdc) frdcs | Coq co -> pp_auxiliary_list_rules fd m xd frdcs; - output_string fd "(** definitions *)\n"; + output_string fd "(* definitions *)\n"; List.iter (fun frdc -> pp_fun_or_reln_defnclass fd m xd lookup frdc) frdcs; | Tex _ -> output_string fd "% defnss\n"; diff --git a/src/grammar_pp.ml b/src/grammar_pp.ml index 022f697..6743c20 100644 --- a/src/grammar_pp.ml +++ b/src/grammar_pp.ml @@ -1401,8 +1401,7 @@ and pp_com_es m xd homs es = ^ String.concat "" (apply_hom_spec m xd hs ((*List.map (function s -> "$"^s^"$")*) ss)) ^ "}" | Isa _ -> " \\ \\" ^ String.concat "" (apply_hom_spec m xd hs ss) ^ "\\" - | Coq _ -> " (*r " ^ String.concat "" (apply_hom_spec m xd hs ss) ^ " *)" - | Hol _ | Lem _ | Caml _ | Lex _ -> " (* " ^ String.concat "" (apply_hom_spec m xd hs ss) ^ " *)" + | Coq _ | Hol _ | Lem _ | Caml _ | Lex _ -> " (* " ^ String.concat "" (apply_hom_spec m xd hs ss) ^ " *)" | Menhir _ -> "/* " ^ String.concat "" (apply_hom_spec m xd hs ss) ^ " */" | Ascii _ | Twf _ -> "" @@ -1416,8 +1415,7 @@ and pp_com_strings m xd homs ss = ^ String.concat "" (apply_hom_spec m xd hs (List.map (function s -> "$"^s^"$") ss)) ^ "}" | Isa _ -> " \\ \\" ^ String.concat "" (apply_hom_spec m xd hs ss) ^ "\\" - | Coq _ -> " (*r " ^ String.concat "" (apply_hom_spec m xd hs ss) ^ " *)" - | Hol _ | Lem _ | Caml _ | Lex _ -> " (* " ^ String.concat "" (apply_hom_spec m xd hs ss) ^ " *)" + | Coq _ | Hol _ | Lem _ | Caml _ | Lex _ -> " (* " ^ String.concat "" (apply_hom_spec m xd hs ss) ^ " *)" | Menhir _ -> "/* " ^ String.concat "" (apply_hom_spec m xd hs ss) ^ " */" | Ascii _ | Twf _ -> ""