add documentation and revision history on coq-notation hom

ott-lang · Dec 28, 2024 · 8a46822 · 8a46822
1 parent 9fd9d8d
commit 8a46822
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 0 deletions.
diff --git a/doc/top2.mng b/doc/top2.mng
@@ -3612,6 +3612,7 @@ file. The table below summarises their meanings.  A \tick{} indicates that argum
 \mykw{tex} & \tick & \myLaTeX{} typesetting for symbolic variables \\
 \mykw{com} &       & comment to appear in \myLaTeX{} syntax definition \\
 \mykw{coq-equality} & & Coq proof script to decide equality over the representation type \\
+\mykw{coq-notation} & & Coq sentence using \texttt{Notation} for the representation type \\
 \mykw{coq-universe} & & Coq universe (e.g.~\texttt{Type}) for the representation type  \\
 \mykw{repr-locally-nameless} & & (Coq only) use a locally-nameless representation \\
 \mykw{phantom} & & suppress the representation type definition in theorem prover output \\
@@ -3637,6 +3638,7 @@ file. The table below summarises their meanings.  A \tick{} indicates that argum
 \mykw{tex} & \tick & \myLaTeX{} typesetting for symbolic variables \\
 \mykw{com} & \tick & comment to appear in \myLaTeX{} syntax definition \\
 \mykw{coq-equality} & & Coq proof script to decide equality over the representation type \\
+\mykw{coq-notation} & & Coq sentence using \texttt{Notation} for the representation type \\
 \mykw{coq-universe} & & Coq universe (e.g.~\texttt{Type}) for the representation type  \\
 \mykw{phantom} & & suppress the representation type definition in theorem prover output \\
 \mykw{aux} & (\tick)& construct an auxiliary grammar rule with a single production \\

diff --git a/revision_history.txt b/revision_history.txt
@@ -575,3 +575,5 @@ Peter Sewell + Thibaut Pérami: Add "menhir-start-type" hom to specify the top l
 2024-12 @palmskog: add explicit locality to generated Coq Hint commands
 
 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
Original file line number	Diff line number	Diff line change
Expand Up		@@ -575,3 +575,5 @@ Peter Sewell + Thibaut Pérami: Add "menhir-start-type" hom to specify the top l
		2024-12 @palmskog: add explicit locality to generated Coq Hint commands

		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