split fails with Error: Refiner was given an argument "(objC * 0)%type" of type "Type" instead of "Set".

[JasonGross]

The code at https://gist.github.com/JasonGross/4956482 gives me a failure on split with Error: Refiner was given an argument "(objC * 0)%type" of type "Type" instead of "Set". I think this is different from issue #7 , since the split code there seems to work now. I'll try to trim this down shortly.

[JasonGross]

Here's a smaller version which reproduces the error:

Set Implicit Arguments.
Generalizable All Variables.

Polymorphic Record Category (obj : Type) :=.

Polymorphic Record Functor objC (C : Category objC) objD (D : Category objD) :=.

Polymorphic Definition ComposeFunctors objC C objD D objE E (G : @Functor objD D objE E) (F : @Functor objC C objD D) : Functor C E.
Admitted.

Polymorphic Definition ProductCategory objC (C : Category objC) objD (D : Category objD) : @Category (objC * objD)%type.
Admitted.

Polymorphic Definition Cat0 : Category Empty_set.
Admitted.

Set Printing Universes.

Lemma ProductLaw0 objC (C : Category objC) (F : Functor (ProductCategory C Cat0) Cat0) (G : Functor Cat0 (ProductCategory C Cat0)) x y :
  ComposeFunctors F G = x /\
  ComposeFunctors G F = y.
Proof.
  split.

[mattam82]

No longer applies.