From 2cfa65014bf1b57a168f0fd6ef71c6663361e23d 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 --- revision_history.txt | 2 ++ src/defns.ml | 2 +- src/grammar_pp.ml | 6 ++---- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/revision_history.txt b/revision_history.txt index 7dd0801..635de14 100644 --- a/revision_history.txt +++ b/revision_history.txt @@ -577,3 +577,5 @@ Peter Sewell + Thibaut Pérami: Add "menhir-start-type" hom to specify the top l 2024-12 @palmskog: move y2l to non-aux directory to avoid Windows problems, fix doc build 2024-12 @palmskog: add coq-notation hom to allow using Coq Notation sentences instead of Definition + +2024-12 @palmskog: only output plain comments in generated Coq code 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 _ -> ""