The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Thanks, Pierre, but this had already been spotted and fixed some time ago ;-)

It should look better once Coq 8.9.0 is released and the manual is updated (whenever that is).

Théo

Le jeu. 10 janv. 2019 à 08:44, Pierre Courtieu <pierre.courtieu AT gmail.com> a écrit :

Hi

Well spotted, there seems to be an inconsistency in the format in the documentation. Ident needs to be green everywhere.

Pierre

PS to Coq dev team: I will submit a PR to fix this

Pierre

 

---

De : coq-club-request AT inria.fr de la part de Jeremy Dawson <jeremy.dawson AT anu.edu.au>
Envoyé : jeudi, janvier 10, 2019 1:25 AM
À : coq-club AT inria.fr
Objet : Re: [Coq-Club] using a hypothesis

 

Hi all,

thanks for all the replies, all seem helpful, but I'm trying to analyse
what they are doing, with the help fo the documentation.

At
https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacv.specialize
it lists
Variant specialize (ident term*) as intro_pattern
with the word ident in bold black type.
Elsewhere bold black type seems to indicate sutff which should be typed
in literally, but here it looks as though this isn't so.
Is this an error in the documentation?

Cheers,

Jeremy