Module Auto_ind_decl

This file is about the automatic generation of schemes about decidable equality,

Oct 2007

Build boolean equality of a block of mutual inductive types
exception EqNotFound of Names.inductive
exception EqUnknown of string
exception UndefinedCst of string
exception InductiveWithProduct
exception InductiveWithSort
exception ParameterWithoutEquality of Names.GlobRef.t
exception NonSingletonProp of Names.inductive
exception DecidabilityMutualNotSupported
exception NoDecidabilityCoInductive
exception ConstructorWithNonParametricInductiveType of Names.inductive
exception DecidabilityIndicesNotSupported
exception InternalDependencies
Build decidability of equality
val eq_dec_scheme_kind : Ind_tables.mutual Ind_tables.scheme_kind