package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type existential_name = Names.Id.t
type cases_pattern_r =
  1. | PatVar of Names.Name.t
  2. | PatCstr of Names.constructor * cases_pattern list * Names.Name.t
and cases_pattern = cases_pattern_r CAst.t
and glob_constr = glob_constr_r CAst.t
and fix_recursion_order =
  1. | GStructRec
  2. | GWfRec of glob_constr
  3. | GMeasureRec of glob_constr * glob_constr option
and fix_kind =
  1. | GFix of (int option * fix_recursion_order) array * int
  2. | GCoFix of int
and predicate_pattern = Names.Name.t * (Names.inductive * Names.Name.t list) Loc.located option
and tomatch_tuple = glob_constr * predicate_pattern
and tomatch_tuples = tomatch_tuple list
and cases_clause = (Names.Id.t list * cases_pattern list * glob_constr) Loc.located
and cases_clauses = cases_clause list
type extended_glob_local_binder_r =
  1. | GLocalAssum of Names.Name.t * Decl_kinds.binding_kind * glob_constr
  2. | GLocalDef of Names.Name.t * Decl_kinds.binding_kind * glob_constr * glob_constr option
  3. | GLocalPattern of cases_pattern * Names.Id.t list * Names.Id.t * Decl_kinds.binding_kind * glob_constr
and extended_glob_local_binder = extended_glob_local_binder_r CAst.t
and closed_glob_constr = {
  1. closure : closure;
  2. term : glob_constr;
}
type uconstr_var_map = closed_glob_constr Names.Id.Map.t
type unbound_ltac_var_map = Geninterp.Val.t Names.Id.Map.t
type ltac_var_map = {
  1. ltac_constrs : var_map;
  2. ltac_uconstrs : uconstr_var_map;
  3. ltac_idents : Names.Id.t Names.Id.Map.t;
  4. ltac_genargs : unbound_ltac_var_map;
}
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct