The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

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?

Best regards,

Michael

>>> SigTest.v starts here <<<

Print sig.

(*
Query commands should not be inserted in
scripts
Inductive sig (A : Type) (P : A -> Prop) : Type :=
    exist : forall x : A, P x -> {x : A | P x}

For sig: Argument A is implicit
For exist: Argument A is implicit
For sig: Argument scopes are [type_scope type_scope]
For exist: Argument scopes are [type_scope function_scope _ _]
*)

Inductive sig2 {A:Type} (P:A -> Prop) : Type :=
    exist2 : forall x:A, P x -> sig2 P.

Print sig2.

(*
Query commands should not be inserted in
scripts
Inductive sig2 (A : Type) (P : A -> Prop) : Type :=
    exist2 : forall x : A, P x -> sig2 P

For sig2: Argument A is implicit and maximally inserted
For exist2: Argument A is implicit and maximally inserted
For sig2: Argument scopes are [type_scope function_scope]
For exist2: Argument scopes are [type_scope function_scope _ _]
*)

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928