コック表記形式がドキュメントによれば

Question

ブレース、一つは印刷表記のためのフォーマットを定義することができる：それは非常に不明瞭である

Notation " '[[' a ']]' b " := (* something *). 

： https://coq.inria.fr/refman/Reference-Manual014.html#sec530

を但し、一方が等の表記法を定義することができ両者が相互作用できるかどうか。しよう：それは正方形ブレースはの一つ、v、及びhvが続くことを期待するように、例えば

format " '[hv' '[[' a ']]' ']' b " 

は、コックをトリップ。

他の種類のエスケープ私はこれまで、Coqが表記法と一致しない形式を拒否してしまった。

私はこれを行うことができるかわからない...

Answer 1

あなたがコード内で見ることができるようにここにあなたの友人がmetasyntax:parse_formathttps://github.com/coq/coq/blob/trunk/toplevel/metasyntax.ml#L102

で、あなたの具体的なスキームは、仕事に行くのではありません。私はいくつかの特定のハックがあるかもしれないなら、今はあなたが二重括弧を使って脱調しなければならないと思う。

[[のケースをparse_quotedに追加するパッチは、Coq上流側とみなされます。

CEP＃9は真のボックスベースのモデルへの非解析を置き換える/進化させることを提案しようとします。