From 8a46822ce42fa5eef94c8c07fb7c7b1574101e97 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sat, 28 Dec 2024 17:03:36 +0100 Subject: [PATCH] add documentation and revision history on coq-notation hom --- doc/top2.mng | 2 ++ revision_history.txt | 2 ++ 2 files changed, 4 insertions(+) diff --git a/doc/top2.mng b/doc/top2.mng index 3923ad3..b243dd3 100644 --- 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 index 157a6ba..7dd0801 100644 --- 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