The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

You can more or less do it with the "Notation" system.

For instance, you can define:

Inductive short :=
 Short : forall (z : Z), compare z -32768 = Ge ->
                              compare z 32768 = Lt -> short.

Notation "a ∷ z ∷ b" := (Short z a b) (at level …).

Notation "⟦ z ⟧" := (Short z _ _).

Now when you want to build the 'short' 3, you can write it
''(eq_refl _)∷3∷(eq_refl _)". But when it is printed by Coq, you will only get
"⟦3⟧" (without the annoying "eq_refl").

I think there are options like "only-printing" or something like that which can be passed to the "Notation …".

That can probably be adapted to your case.

2013/9/11 t x <txrev319 AT gmail.com>

Hi,

  Without delving into OCaml, is it possible to write my own "pretty-printing" routine in Coq?

  What I mean is as follows: when looking at the goal state, besides toggling certain options, I have absolutely no control over how the Hypothesis and Conclusion is displayed.

  For complicated situations (a Record containing a list of other Records), I would like to have a bit more control over what is displayed and what is not displayed.

  Basically, I want to be able to write a function of type (Gallina Term -> list string).

  I'm also using proof general. If others have run into this problem and found that hacking at the elisp layer to rewrite the buffer, advice from that would be helpful too.

Thanks!

--
.../Sedrikov\...