coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: Pierre Courtieu <Pierre.Courtieu AT cnam.fr>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?
Date: Thu, 2 Apr 2020 11:55:51 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk1-f176.google.com
Ironport-phdr: 9a23:/9Bt1BUNE5aDSNPxQUrlqYRIEXjV8LGtZVwlr6E/grcLSJyIuqrYZhWHt8tkgFKBZ4jH8fUM07OQ6P+wHzFYqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aMlzFOAF0PuX4HJLJx4Tyjrjqus6bXwIdvDuwe6l/ZD6xsB/Nt8QLyd9aK6sr0BaPiXxVYfhXyH5ALlSamlDy/JHj0oRk9nEaufUn9s1NVaj3V6s9RL1cSj8hNip9sM/ssxjAQA+C61MTV2wXllxDBA2Tv0KyZYv4riav7rk14yKdJ8CjCOlsAW3zvZcucwfhjWI8DxB89WjWjsJqi6cC+UCuohV+x8jfZ4THbaMiLJOYRssTQC96ZugUTzZIW9ruYI4GDu5HNuFd/dGk+gk+6CCmDAzpP9vBjz9Fgnisg/8/2uUlVBjFhUkuRo1Q9nvTq9rxOeEZVuXnlKQ=

On Thu, 2 Apr 2020 11:23:31 -0400
"jonikelee AT gmail.com"

<jonikelee AT gmail.com>
wrote:

> On Thu, 2 Apr 2020 10:45:49 +0200
> Pierre Courtieu
> <Pierre.Courtieu AT cnam.fr>
> wrote:
>
> > Nice ltac!
> > I have something similar in LibHyps without touching the proof term
> > (thanks to ltac hack from J.Leivant).
>
> Here's the source for that hypothesis harvesting and iteration hack:
> https://github.com/jonleivent/mindless-coding-phase2/blob/master/hypiter.v

Somewhere, I had a version of this hack that grouped like-typed
hypotheses together to take full advantage of ProofGeneral's ability to
list adjacent like-typed hypotheses on the same line. I'll look for it...

[Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Agnishom Chattopadhyay, 04/01/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Samuel Gruetter, 04/02/2020
  - Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Pierre Courtieu, 04/02/2020
    - Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, jonikelee AT gmail.com, 04/02/2020
      - Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, jonikelee AT gmail.com, 04/02/2020
        
        Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, jonikelee AT gmail.com, 04/02/2020
        
        Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Pierre Courtieu, 04/02/2020
        
        Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, jonikelee AT gmail.com, 04/03/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Paolo Giarrusso, 04/09/2020
  - Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Agnishom Chattopadhyay, 04/10/2020
    - Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Paolo Giarrusso, 04/10/2020