The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 18/09/2017 09:53, Soegtrop, Michael wrote:
> Dear Guillaume,
> 
>> I cannot reproduce your issue. I tried with 8.5, 8.6, and 8.7, and they 
>> all agree
>> that all the arguments lie in scope type_scope. This is consistent with
> 
> Interesting. On Windows in CoqIDE with Coq 8.6 and 8.6.1 (using a fresh 
> install using the official installers with no environment changes) I get 
> the below behavior. What exact version did you use?

Opam packages compiled on Linux:

$ echo "Print sig. Print sig2." | ..../coqtop

Welcome to Coq 8.4pl6 (December 2016)
Welcome to Coq 8.5pl3 (September 2017)
Welcome to Coq 8.6.1 (July 2017)
Welcome to Coq 8.7+beta1 (September 2017)
...
For sig: Argument scopes are [type_scope type_scope]
...
For sig2: Argument scopes are [type_scope type_scope type_scope]
...

There are some variations for exist and exist2, with _ instead of
function_scope sometimes. But for sig and sig2, all the versions of Coq
that I tested behave consistently.

Best regards,

Guillaume