coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] [SUSPECTED SPAM] Re: "Sequence is associative." (?)

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] [SUSPECTED SPAM] Re: "Sequence is associative." (?)
Date: Thu, 31 Jan 2019 00:09:32 +0000
Accept-language: en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-SY3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:XlSNBxIPDVldrOjTbtmcpTZWNBhigK39O0sv0rFitYgeLfrxwZ3uMQTl6Ol3ixeRBMOHs6IC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwZFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhicZOTAk7GHZhM9+jKxZrxKguxNxzIHbbZqJNPVlZK7RYc8WSXZDU8tXSidPApm8b4wKD+cZOehXsZP9qEULrRq+GAKiCvngyzFThn/x260xzuMsHwXY0ww6Ad0OtXTVoM/7OqgIX+G1167IzTPYYvxM3zf99ZLEfQ48rvGRR75/a9fRxFApGgjYjVuQsZToMjyJ2ugXrmSX8+htWfiyh2MpqQx9uCWjytkjh4XRm44YykzI+T9nzIopK9C0UlB3bcO4HJdKqi2XOY97TtssQ252uys21rgLtJu/cSUJ05sqyBvSZ+GJfoeW/x3uUeiRLil7iX55fb+zmQ298Uavx+D6S8K6ykxFrjBfndnJrn0N1wLc6syASvZl4kqu1yuB2xzO5u1dPE47l6TWJ4cmwrEriJUfq0PDHjLqmErti6+Wa0Mk9fWy5+T/eLXmoYOcOJFohQHiM6Quncq/Df4/MggTQ2ib/eO81Lrg/UHjXLpKifg2nrHYsJDcO8sbura0DgBJ3oo59hqzEzWr3M4FkXQJLl9JYg+Lg5bmNl3WJfD3F/a/g1CikDdxwPDGO6XsDJHTIXjZjrjheLZ851RSxgUpw9Ff/JVUCrcaLf3pXE/xqcbUAQEkPAyp2eroEsh92psEWW2TGq+ZLL/SsViQ6+0zJOmMfZYZtyr5K/g4/PHjlmQ5mF8Yfamxx5QbcnG4HvJ8I0WYe3XgmNkBEX1Z9jY5Gabhj0THWjpObV6zWbg973c1EsjuWYzEX8WmhKGL9Ca9BJxfIG5cXAOiC3DtIqeJQfoJeWq+K9B6lTpMAZqsUYIkxFeCvRDhzLxPJ+zJvCAUqNTqyY4mtKXoiRgu+GksXIym2GaXQjQsxzJad3oNxKl65HdF5BKG2Kl8jeZfEIUJtfpPT0E3OYOaxvEoUomuCDKERc+ATROdevvjGSs4F4hjytkTJUtxBpOrk0Kbhnf4M/ouj7WOQacM3Ofc0nz2e5kv4kv9jPBktGh9B8xFOCuhm7J18BXVC8jRiUKFmq22dKMaminQ6GOEymnIt0ZdAld9

On 29/1/19 3:41 am, Pierre Courtieu wrote:
> all:tac. applies the tac to all goals.
> Period.

Well, IMRO this is pretty unsatisfactory. Since the order of applying
tactics (or parts of them) to subgoals matters (as in the case, for
example, of instantiating existential variables) you are making it seem
that coq's design is so complicated that it is not worth while trying to
describe it.

And there is certainly nothing in the documentation, as far as I can
see, to explain, or even to alert the user to the fact that
all : solve_eqs
when there are two subgoals, solves both, whereas
all : repeat solve_eqs
leaves one of them unsolved

Cheers,

Jeremy

Re: [Coq-Club] "Sequence is associative." (?), (continued)