coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Strange subtyping

From: Stefan Monnier <monnier AT IRO.UMontreal.CA>
To: Maxime Dénès <mail AT maximedenes.fr>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Strange subtyping
Date: Thu, 07 Jun 2018 11:33:09 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=monnier AT IRO.UMontreal.CA; spf=Pass smtp.mailfrom=monnier AT iro.umontreal.ca; spf=None smtp.helo=postmaster AT pruche.dit.umontreal.ca
Ironport-phdr: 9a23:eLQlbB+r1gX0B/9uRHKM819IXTAuvvDOBiVQ1KB41OgcTK2v8tzYMVDF4r011RmVBdids6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+553ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRh/2hikaNDA5/m/Zhc5+g61UvB2svAB/z5LObY2JKPZzZL/RcNUHTmRBRMZRUClBD5uhYYsTEeUBM/xXr4/grFUJqhu+Aw+sBOLxxT9Sm3T72qg60+MnEQHA3QwvAcgOvW/XotvpLakeS+66wq7PzTXFc/NWwyny55LMchw7v/yBQat9fMzMwkcsDwPIlkicpIL7Mz+PyOgBr2eW4/B+We+gimMrsR99ria3yssxhITFmJgZxk7Y+Sh22oo5O9+1RFRlbdOrDpddsTyROZFsTcM4WW5ovT43yr0Ytp6/eygH0IwnxwTCa/Obc4iH/AjvW/uQITdknn5lZbe/hxG08Ui80O3zSNO70FJQoiVZiNbArnEN1xrN5cibUvZx40ms1SiV2wzN9u1JLlo4mbTUJpMg2LI8iIQfvVzGHiDsmUX2iKGWdl8j+uit8+nnZ7LmppmaN491lA7+KL8jms2lAeQ/KAQOQm2b+eO61L3/5032Xq9FjvksnqbFqp/WPd4bqbKhAw9JzoYj7A6yACuh0NQBhHUIMFZFeA+cgIXyIFHPIPX4De+ljFi2kTdrwerGPrz7DZnXIHjDiuSpQbEozkdMyQ8+hfze4RJPQuUEKfP3ckr4pN3dAxM0NQGvhej9XoZTzIQbDFmTD6GQNuv3tlmO5+81a72JY4kTuTvnA9kfwLjTqHg/hUUQdK3v9rJBOyPwJehvP0jMOSmkudwGC2pf5lNvHtyvs0WLVHtoX1j3Wqs94j8hD4f/XdXCXIfrnbmG2juhE5RSIGtPWAnVTSXYMr6cUvJJUxq8Z9d7m2VUB5mbbMkc8BaoqBX3wr4hBcOGonRF56Km78B84qjorT939TFwCJ7AgXmXUmp0kyUERiNwwaV4p1Bnx16Hl6Nx0aRV

> I'm not sure why we would keep Set in your proposal, though. Does it
> play any role?

Support the many lines of existing Coq code which mention Set?

Stefan

[Coq-Club] Strange subtyping, Helmut Brandl, 06/07/2018
- Re: [Coq-Club] Strange subtyping, Matthieu Sozeau, 06/07/2018
  - Re: [Coq-Club] Strange subtyping, Stefan Monnier, 06/07/2018
    - Re: [Coq-Club] Strange subtyping, Maxime Dénès, 06/07/2018
      - Re: [Coq-Club] Strange subtyping, Stefan Monnier, 06/07/2018
        
        Re: [Coq-Club] Strange subtyping, Maxime Dénès, 06/07/2018
  - Re: [Coq-Club] Strange subtyping, Helmut Brandl, 06/07/2018
  - Re: [Coq-Club] Strange subtyping, Helmut Brandl, 06/09/2018
    - Re: [Coq-Club] Strange subtyping, Théo Zimmermann, 06/09/2018
      - Re: [Coq-Club] Strange subtyping, Helmut Brandl, 06/15/2018