coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Rewriting with equivalence relations in Set / Type

From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Rewriting with equivalence relations in Set / Type
Date: Fri, 28 Feb 2014 00:01:33 +0100

On 27/02/2014 23:53, Jason Gross wrote:
> I believe it was requested and might be planed, but not yet implemented.

In trunk, there is an undocumented command (that one should not use):

%< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %<

Parameter bla : forall m : nat, m = m.

Hint Resolve bla : foo.

Print HintDb foo.

Remove Hints bla : foo.

Print HintDb foo.

%< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %<

This only works with hints associated to a name, and I personnally find
it dangerous to use, but at least it's here to hack around.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] Rewriting with equivalence relations in Set / Type, Rui Baptista, 02/27/2014
- <Possible follow-up(s)>
- [Coq-Club] Rewriting with equivalence relations in Set / Type, Rui Baptista, 02/27/2014
  - Re: [Coq-Club] Rewriting with equivalence relations in Set / Type, Jason Gross, 02/27/2014
    - Re: [Coq-Club] Rewriting with equivalence relations in Set / Type, Rui Baptista, 02/27/2014
      - Re: [Coq-Club] Rewriting with equivalence relations in Set / Type, Rui Baptista, 02/27/2014
      - Re: [Coq-Club] Rewriting with equivalence relations in Set / Type, Jason Gross, 02/27/2014
        
        Re: [Coq-Club] Rewriting with equivalence relations in Set / Type, Pierre-Marie Pédrot, 02/28/2014
        
        Re: [Coq-Club] Rewriting with equivalence relations in Set / Type, Rui Baptista, 02/28/2014
      - Re: [Coq-Club] Rewriting with equivalence relations in Set / Type, Robbert Krebbers, 02/28/2014