Merge pull request #121 from ott-lang/fix-coq-comments

only output plain comments in generated Coq code
ott-lang · Dec 30, 2024 · 8ce440c · 8ce440c
2 parents a14906c + 2cfa650
commit 8ce440c
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 5 deletions.
diff --git 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
@@ -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
@@ -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 _ -> " \\<comment> \\<open>" ^ String.concat "" (apply_hom_spec m xd hs ss) ^ "\\<close>"
-    | 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 _ -> " \\<comment> \\<open>" ^ String.concat "" (apply_hom_spec m xd hs ss) ^ "\\<close>"
-    | 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 _ -> ""
Original file line number	Diff line number	Diff line change
Expand Up		@@ -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