package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
exception EqNotFound of Names.inductive * 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
val eq_dec_scheme_kind : Ind_tables.mutual Ind_tables.scheme_kind
val make_eq_decidability : Ind_tables.mutual_scheme_object_function