coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] using a hypothesis

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>, "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] using a hypothesis
Date: Thu, 10 Jan 2019 07:43:48 +0000
Accept-language: fr-FR, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr1-f49.google.com
Ironport-phdr: 9a23:gnqQKh2UBF+S5EnusmDT+DRfVm0co7zxezQtwd8ZseITKPad9pjvdHbS+e9qxAeQG9mDu7Qc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPYAhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmiDkJOSMl8G/ZicJwgqBUrw6uqBFk2YHYfI6aOeBicq/BYN8XQ3dKUMZLVyxGB4Oxd5EBD+sfMuZCtYnyuUYFoAW5BQmxHuPv1j5IiWHr3aYn1OkhCQDG0xI6H9IUrnvYtsn6NKAPUeCv0KnIzCvMb+5N1Dfy7YjHaBEhofWWUb1sdsrRzFAiGgXYhVuerozlOima1uULs2WD7upgU/ivi289pA1rrDiv3MEhgZTKiIIN0l3I6zl1zYIvKdC7SEN3e8CoHIVNuy2AOIZ7RtsuTm50tCog17EKpYO3cDIOxZg63RLSa/KKfo6V6Rz5TumROy13hHd9dbK/mRmy9U+gx/X5Vsau0VZKqjNJk9fWtnwQzhDT5MeKR/9n8keu3jaP0A/T6uVaLkwuiaXbLJshzqYxlpoVr0vDAjf7lFvqgKKSbEkp+eil5/75brn4u5OQLYB5hwXmPqQrgMO/AOA4MgYUX2ic/OSxzKXj/UznT7VQlP05jLPVv4zdJcQGvK65Hw5V3Zg+6xukADem1c4XnXgDLF5fZB2HiI3pN0nUIP/kFfe/n0iskDBzyv/aOb3hG4zBIWTHkLf8Zrlw8FVcyQo2zdBH/Z1YELABIPTpWk/wrtPUFBE5Mxbni9rgXZ920ZpbUmaSCIeYNrnTuBmG/Khnd+KLfcoevCv3A/kj/f/ny3EjzxtVN6KuxN4cbG2yNvVgOUSQJ3T2yJ9VGmAT+wE6UebCiVuYUDcVaWzkDIwm4TRuMIOrF53ODquqnaad3SqmVslOZ21cEF3KGnD1bZmFVuokZyebI8snmTsBA+vyA7Q93A2j4Vepg4FsKfDZr3VB5MDTkeNt7uiWrikcsDl9DsCTyWaIFjgmkWYBRjtw16d68xUklgWzlJNgivkdLuR9outTW15jZ5HZxu1+Tdv1X1CZJ4rbeBOdWtyjRAoJYJcxztsJORsvHtyjilXcxXPvDeNE0bOMA5Mw/+TX2H2jf8s=

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

[Coq-Club] using a hypothesis, Jeremy Dawson, 01/08/2019
- Re: [Coq-Club] using a hypothesis, Li-yao Xia, 01/08/2019
  - Re: [Coq-Club] using a hypothesis, Jeremy Dawson, 01/10/2019
    - Re: [Coq-Club] using a hypothesis, Pierre Courtieu, 01/10/2019
      - Re: [Coq-Club] using a hypothesis, Théo Zimmermann, 01/11/2019
- Re: [Coq-Club] using a hypothesis, Lily Chung, 01/08/2019
- Re: [Coq-Club] using a hypothesis, Marko Doko, 01/08/2019
  - Re: [Coq-Club] using a hypothesis, Théo Zimmermann, 01/08/2019