The Coq mailing list

[<michael.soegtrop AT intel.com>]

Dear Coq users,

I have a problem with implicit record type arguments defined via {} binders.
Print and Print Implicit show different status on wether such parameters are
implicit or not, and it doesn't work as expected. Please have a look at the
Coq code below. Is therer an explanation for this behaviour, or is this a bug?

Best regards,

Michael


Record RecTest {par : nat} : Type := mkRecTest
{
  elem1 : nat
}.

Print mkRecTest.

(*
Record RecTest (par : nat) : Type := mkRecTest { elem1 : nat }

For RecTest: Argument par is implicit and maximally inserted
For RecTest: Argument scope is [nat_scope]
For mkRecTest: Argument scopes are [nat_scope nat_scope]

=> This is what I expected
*)

Print Implicit mkRecTest.

(*
mkRecTest : forall par : nat, nat -> RecTest

=> Here par is not mentioned as implicit
=> Also I have to give the argument explicitly
*)

Definition test : @RecTest 1 := mkRecTest _ 1.

(* Define par more explicitly as implicit *)

Arguments mkRecTest [par] _.

Print mkRecTest.

(*
Record RecTest (par : nat) : Type := mkRecTest { elem1 : nat }

For RecTest: Argument par is implicit and maximally inserted
For mkRecTest: Argument par is implicit
For RecTest: Argument scope is [nat_scope]
For mkRecTest: Argument scopes are [nat_scope nat_scope]
*)

Print Implicit mkRecTest.

(*
mkRecTest : forall par : nat, nat -> RecTest

Argument par is implicit
*)

Definition test2 : @RecTest 1 := mkRecTest 1.

(* => Now everything works fine *)