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
val eq_dec_scheme_kind : Ind_tables.mutual Ind_tables.scheme_kind
val make_eq_decidability : Ind_tables.mutual_scheme_object_function