coq 8.8.2 · OCaml Package

type existential_name = Names.Id.t

type !'a cases_pattern_r =

and !'a cases_pattern_g = ('a cases_pattern_r, 'a) DAst.t

type cases_pattern = [ `any ] cases_pattern_g

type !'a glob_constr_r =

and !'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t

and !'a glob_decl_g =
  Names.Name.t
  * Decl_kinds.binding_kind
  * 'a glob_constr_g option
  * 'a glob_constr_g

and !'a fix_recursion_order_g =

and !'a fix_kind_g =

and 'a predicate_pattern_g =
  Names.Name.t * (Names.inductive * Names.Name.t list) CAst.t option

and !'a tomatch_tuple_g = 'a glob_constr_g * 'a predicate_pattern_g

and !'a tomatch_tuples_g = 'a tomatch_tuple_g list

and !'a cases_clause_g =
  (Names.Id.t list * 'a cases_pattern_g list * 'a glob_constr_g) CAst.t

and !'a cases_clauses_g = 'a cases_clause_g list

type glob_constr = [ `any ] glob_constr_g

type tomatch_tuple = [ `any ] tomatch_tuple_g

type tomatch_tuples = [ `any ] tomatch_tuples_g

type cases_clause = [ `any ] cases_clause_g

type cases_clauses = [ `any ] cases_clauses_g

type glob_decl = [ `any ] glob_decl_g

type fix_kind = [ `any ] fix_kind_g

type predicate_pattern = [ `any ] predicate_pattern_g

type fix_recursion_order = [ `any ] fix_recursion_order_g

type any_glob_constr =

type !'a disjunctive_cases_clause_g =
  (Names.Id.t list * 'a cases_pattern_g list list * 'a glob_constr_g) CAst.t

type !'a disjunctive_cases_clauses_g = 'a disjunctive_cases_clause_g list

type !'a cases_pattern_disjunction_g = 'a cases_pattern_g list

type disjunctive_cases_clause = [ `any ] disjunctive_cases_clause_g

type disjunctive_cases_clauses = [ `any ] disjunctive_cases_clauses_g

type cases_pattern_disjunction = [ `any ] cases_pattern_disjunction_g

type !'a extended_glob_local_binder_r =

and !'a extended_glob_local_binder_g =
  ('a extended_glob_local_binder_r, 'a) DAst.t

type extended_glob_local_binder = [ `any ] extended_glob_local_binder_g

package coq