coq 8.7.2 · OCaml Package

type !'a matching_function = Evd.evar_map -> EConstr.constr -> 'a option

type testing_function = Evd.evar_map -> EConstr.constr -> bool

val match_with_non_recursive_type : 
  (EConstr.constr * EConstr.constr list) matching_function

val is_non_recursive_type : testing_function

val match_with_disjunction : 
  ?strict:bool ->
  ?onlybinary:bool ->
  (EConstr.constr * EConstr.constr list) matching_function

val is_disjunction : ?strict:bool -> ?onlybinary:bool -> testing_function

val match_with_conjunction : 
  ?strict:bool ->
  ?onlybinary:bool ->
  (EConstr.constr * EConstr.constr list) matching_function

val is_conjunction : ?strict:bool -> ?onlybinary:bool -> testing_function

val match_with_record : 
  (EConstr.constr * EConstr.constr list) matching_function

val is_record : testing_function

val match_with_tuple : 
  (EConstr.constr * EConstr.constr list * bool) matching_function

val is_tuple : testing_function

val match_with_empty_type : EConstr.constr matching_function

val is_empty_type : testing_function

val match_with_unit_or_eq_type : EConstr.constr matching_function

val is_unit_or_eq_type : testing_function

val is_unit_type : testing_function

val is_inductive_equality : Names.inductive -> bool

val match_with_equality_type : 
  (EConstr.constr * EConstr.constr list) matching_function

val is_equality_type : testing_function

val match_with_nottype : (EConstr.constr * EConstr.constr) matching_function

val is_nottype : testing_function

val match_with_forall_term : 
  (Names.Name.t * EConstr.constr * EConstr.constr) matching_function

val is_forall_term : testing_function

val match_with_imp_term : (EConstr.constr * EConstr.constr) matching_function

val is_imp_term : testing_function

val has_nodep_prod_after : int -> testing_function

val has_nodep_prod : testing_function

val match_with_nodep_ind : 
  (EConstr.constr * EConstr.constr list * int) matching_function

val is_nodep_ind : testing_function

val match_with_sigma_type : 
  (EConstr.constr * EConstr.constr list) matching_function

val is_sigma_type : testing_function

type equation_kind =

| MonomorphicLeibnizEq of EConstr.constr * EConstr.constr
| PolymorphicLeibnizEq of EConstr.constr * EConstr.constr * EConstr.constr
| HeterogenousEq of EConstr.constr * EConstr.constr * EConstr.constr * EConstr.constr

exception NoEquationFound

val match_with_equation : 
  Evd.evar_map ->
  EConstr.constr ->
  Coqlib.coq_eq_data option * EConstr.constr * equation_kind

val find_eq_data_decompose : 
  'a Proofview.Goal.t ->
  EConstr.constr ->
  Coqlib.coq_eq_data
  * EConstr.EInstance.t
  * (EConstr.types * EConstr.constr * EConstr.constr)

val find_this_eq_data_decompose : 
  'a Proofview.Goal.t ->
  EConstr.constr ->
  Coqlib.coq_eq_data
  * EConstr.EInstance.t
  * (EConstr.types * EConstr.constr * EConstr.constr)

val find_eq_data : 
  Evd.evar_map ->
  EConstr.constr ->
  Coqlib.coq_eq_data * EConstr.EInstance.t * equation_kind

val find_sigma_data_decompose : 
  Evd.evar_map ->
  EConstr.constr ->
  Coqlib.coq_sigma_data
  * (EConstr.EInstance.t
     * EConstr.constr
     * EConstr.constr
     * EConstr.constr
     * EConstr.constr)

val match_sigma : 
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr * EConstr.constr

val is_matching_sigma : Evd.evar_map -> EConstr.constr -> bool

val match_eqdec : 
  Evd.evar_map ->
  EConstr.constr ->
  bool
  * Globnames.global_reference
  * EConstr.constr
  * EConstr.constr
  * EConstr.constr

val dest_nf_eq : 
  'a Proofview.Goal.t ->
  EConstr.constr ->
  EConstr.constr * EConstr.constr * EConstr.constr

val is_matching_not : Evd.evar_map -> EConstr.constr -> bool

val is_matching_imp_False : Evd.evar_map -> EConstr.constr -> bool

package coq