coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Bug or feature?

From: Beta Ziliani <beta AT mpi-sws.org>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Bug or feature?
Date: Fri, 3 Feb 2017 09:56:49 -0300
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=beta AT mpi-sws.org; spf=Pass smtp.mailfrom=beta AT mpi-sws.org; spf=None smtp.helo=postmaster AT hera.mpi-klsb.mpg.de
Ironport-phdr: 9a23:QQm5lxQLq8dmxMNni+FWM1Tjwdpsv+yvbD5Q0YIujvd0So/mwa69ZRCN2/xhgRfzUJnB7Loc0qyN4vymBjVLvc3JmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanb75/KBq7oR/Tu8ULjodvJag8wQbVr3VVfOhb2XlmLk+JkRbm4cew8p9j8yBOtP8k6sVNT6b0cbkmQLJBFDgpPHw768PttRnYUAuA/WAcXXkMkhpJGAfK8hf3VYrsvyTgt+p93C6aPdDqTb0xRD+v4btnRAPuhSwaLDMy7n3ZhdJsg6JauBKhpgJww4jIYIGOKfFyerrRcc4GSWZdW8pcUTFKDIGhYIsVF+cPPehWoYrgqVUQsRSzHhOjCP/1xzJSmnP6wa833uI8Gg/GxgwgGNcOvWzJodrrKKcdS/2+w6rJzTXHbvNZwzH96InVeR0muv6DQ65wftDKxEkqDwPFj0ycqZfrPjOOzOgNtHKb7+V5WO+plmUpqBlxryCyysoijoTFnJ8Zx1Te+Slk2oo4Ktm1RUhmatC+CpRQrTuVN45uT8MiXW5ovCE6x6UGuZGlZigF0o4rxxvHa/yGaoSI4RbjVP2KLjtigXJlYL2/iwyv/ke+0uH8V8+030hWriddj9XBuHQA2wbO5sWDUPdx412t1DmL2gzL7+FLO0E0la7VK547xb4wk4Ievl/dES/qgkr7l6qWdl0l+uSx8OTmbK7mqoWbN49uhQHyKr4uldCnAeQkLggOWHCW9vi71L365EH2XLFKjuAtnaTCq5DbJcEbprajDANP04Yj7Qy/Dza839gCk3kHNgENRBXSpI/wc3rKPfqwWfy4mhGnlCph7/HAJLzoRJvXeCvtirDkKJxw90cU+gs3zNlZ5toAALwdKdr2Qk60r8PDSBgjPFrnkK7cFNxh29ZGCiq0CaiDPfaX6AfQ6w==

Hi list,

I stumble across what I think is an odd behavior when mixing named and dB contexts, and I’m going to file it as a bug unless someone convinces me that this is a feature:

Section test.
Variable x : nat.

Definition ex := fun x y:nat=>ltac:(exact (x + y)).
Print ex.

outputs

ex = fun _ y : nat => x + y
     : nat -> nat -> nat

I am expecting, of course,

ex = fun x y : nat => x + y
     : nat -> nat -> nat

Note that defining `x` in a Section is important; if I make x a top level variable, the example is constructed as expected.

Best,
Beta

[Coq-Club] Bug or feature?, Beta Ziliani, 02/03/2017
- Re: [Coq-Club] Bug or feature?, Bruno Barras, 02/03/2017
  - Re: [Coq-Club] Bug or feature?, Ralf Jung, 02/03/2017
- Re: [Coq-Club] Bug or feature?, Maxime Dénès, 02/03/2017
  - Re: [Coq-Club] Bug or feature?, Beta Ziliani, 02/03/2017
  - Re: [Coq-Club] Bug or feature?, Beta Ziliani, 02/03/2017
    - Re: [Coq-Club] Bug or feature?, Andreas Abel, 02/05/2017
      - Re: [Coq-Club] Bug or feature?, Beta Ziliani, 02/06/2017