coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Difference between uconstr and open_constr
Date: Wed, 27 Jul 2016 00:23:16 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mailinglists AT robbertkrebbers.nl; spf=None smtp.mailfrom=mailinglists AT robbertkrebbers.nl; spf=None smtp.helo=postmaster AT smtp1.science.ru.nl
Ironport-phdr: 9a23:IBalgRY6CA0iwWgkVPWTKb3/LSx+4OfEezUN459isYplN5qZpcm8bnLW6fgltlLVR4KTs6sC0LuO9f68EjRaqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ3pzxibz5o8ebSj4LrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGwD884mosVHSODxe7kyBehTCy1jOGQo7uXqswPCRE2B/C1PfH8Rl09yBALP4QvmFrTrvyHwu/BmkH2fNMzyTLY7XTW587xDUhjigiodKz0j/Wvdh9ZryqRf9kHy7ydjypLZNdnGfMF1ebnQKIsX

Dear Coq club,

Could someone explain me the difference between the tactic argument types uconstr and open_constr?

Thanks,

Robbert

[Coq-Club] Difference between uconstr and open_constr, Robbert Krebbers, 07/27/2016
- Re: [Coq-Club] Difference between uconstr and open_constr, Jonathan Leivent, 07/27/2016
  - Re: [Coq-Club] Difference between uconstr and open_constr, Jonathan Leivent, 07/27/2016
    - [Coq-Club] Shadowing binders abusively renamed?, Yannick, 07/27/2016
      - Re: [Coq-Club] Shadowing binders abusively renamed?, Jonathan Leivent, 07/27/2016
        
        Re: [Coq-Club] Shadowing binders abusively renamed?, Yannick, 07/27/2016
        
        Re: [Coq-Club] Shadowing binders abusively renamed?, Jonathan Leivent, 07/27/2016
  - Re: [Coq-Club] Difference between uconstr and open_constr, Pierre-Marie Pédrot, 07/27/2016