coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Rewriting with "identity type in Type"

From: Andrej Bauer <andrej.bauer AT andrej.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Rewriting with "identity type in Type"
Date: Mon, 2 Apr 2012 23:31:00 +0200

What's the current status of having Coq "rewrite" working with an
identity type defined in Type rather than in Prop?

There is a patch that accomplishes this, I think (but where)? Are
there plans to include it in a future version?

With kind regards,

Andrej

[Coq-Club] Rewriting with "identity type in Type", Andrej Bauer
- [Coq-Club] Re: Rewriting with "identity type in Type", Andrej Bauer
  - Re: [Coq-Club] Re: Rewriting with "identity type in Type", Jean-Francois Monin
    - Re: [Coq-Club] Re: Rewriting with "identity type in Type", AUGER Cédric
  - Re: [Coq-Club] Re: Rewriting with "identity type in Type", Vladimir Voevodsky
    - Re: [Coq-Club] Re: Rewriting with "identity type in Type", Jean-Francois Monin
    - Re: [Coq-Club] Re: Rewriting with "identity type in Type", Andrej Bauer
      - Re: [Coq-Club] Re: Rewriting with "identity type in Type", Tom Prince