Quelle  Inductive.out   Sprache: unbekannt

File "./output/Inductive.v", line 1, characters 0-93:
The command has indeed failed with message:
In environment
list' : Set -> Set
A : Set
a : A
l : list' A
Unable to unify "list' (A * A)%type" with "list' A".
Inductive foo (A : Type) (x : A) (y : A := x) : Prop :=  Foo : foo A x.

Arguments foo A%_type_scope x
Arguments Foo A%_type_scope x
myprod unit bool
     : Set
option : Type -> Type

option is template universe polymorphic
Arguments option A%_type_scope
Expands to: Inductive Corelib.Init.Datatypes.option
Declared in library Corelib.Init.Datatypes, line 202, characters 10-16
option : Type@{option.u0} -> Type@{max(Set,option.u0)}

option is template universe polymorphic on option.u0 (cannot be instantiated to Prop)
Arguments option A%_type_scope
Expands to: Inductive Corelib.Init.Datatypes.option
Declared in library Corelib.Init.Datatypes, line 202, characters 10-16
File "./output/Inductive.v", line 27, characters 4-13:
The command has indeed failed with message:
Parameters should be syntactically the same for each inductive type.
Type "B" has no parameters
but type "Inductive" has parameters "A".
File "./output/Inductive.v", line 30, characters 6-15:
The command has indeed failed with message:
Parameters should be syntactically the same for each record type.
Type "B" has no parameters
but type "Inductive" has parameters "A".
or : Prop -> Prop -> Prop

or is not universe polymorphic
or may only be eliminated to produce values whose type is SProp or Prop.
Arguments or (A B)%_type_scope
Expands to: Inductive Corelib.Init.Logic.or
Declared in library Corelib.Init.Logic, line 89, characters 10-12
sunit : SProp

sunit is not universe polymorphic
sunit may only be eliminated to produce values whose type is SProp.
Expands to: Inductive Inductive.sunit
Declared in library Inductive, line 38, characters 10-15
sempty@{q ; } : Type@{q ; Set}
(* q ;  |=  *)

sempty is universe polymorphic
sempty@{q ; } may only be eliminated to produce values whose type is in sort quality q,
  unless instantiated such that the quality SProp
  is equal to the instantiation of q, or to qualities smaller
  (SProp <= Prop <= Type, and all variables <= Type)
  than the instantiation of q.
Expands to: Inductive Inductive.sempty
Declared in library Inductive, line 44, characters 22-28
ssig@{q1 q2 q3 ; a b} :
forall A : Type@{q1 ; a}, (A -> Type@{q2 ; b}) -> Type@{q3 ; max(a,b)}
(* q1 q2 q3 ; a b |=  *)

ssig is universe polymorphic
ssig@{q1 q2 q3 ; a b} may only be eliminated to produce values whose type is in sort quality q3,
  unless instantiated such that the qualities q1, q2 and Prop
  are equal to the instantiation of q3, or to qualities smaller
  (SProp <= Prop <= Type, and all variables <= Type)
  than the instantiation of q3.
Arguments ssig A%_type_scope B%_function_scope
Expands to: Inductive Inductive.ssig
Declared in library Inductive, line 48, characters 22-26
BoxP@{q ; a} : Type@{q ; a} -> Prop
(* q ; a |=  *)

BoxP is universe polymorphic
BoxP@{q ; a} may only be eliminated to produce values whose type is SProp or Prop,
  unless instantiated such that the quality q is SProp or Prop.
Arguments BoxP A%_type_scope
Expands to: Inductive Inductive.BoxP
Declared in library Inductive, line 56, characters 22-26