package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
val reset_meta_count : unit -> unit
val new_meta : 'a -> Miniml.ml_type
val type_subst_list : Miniml.ml_type list -> Miniml.ml_type -> Miniml.ml_type
val type_subst_vect : Miniml.ml_type array -> Miniml.ml_type -> Miniml.ml_type
val instantiation : Miniml.ml_schema -> Miniml.ml_type
val needs_magic : (Miniml.ml_type * Miniml.ml_type) -> bool
val put_magic_if : bool -> Miniml.ml_ast -> Miniml.ml_ast
val generalizable : Miniml.ml_ast -> bool
module Mlenv : sig ... end
val type_mem_kn : Names.MutInd.t -> Miniml.ml_type -> bool
val type_maxvar : Miniml.ml_type -> int
val type_decomp : Miniml.ml_type -> Miniml.ml_type list * Miniml.ml_type
val type_recomp : (Miniml.ml_type list * Miniml.ml_type) -> Miniml.ml_type
val var2var' : Miniml.ml_type -> Miniml.ml_type
type abbrev_map = Names.GlobRef.t -> Miniml.ml_type option
val type_expand : abbrev_map -> Miniml.ml_type -> Miniml.ml_type
val type_simpl : Miniml.ml_type -> Miniml.ml_type
val type_to_sign : abbrev_map -> Miniml.ml_type -> Miniml.sign
val type_to_signature : abbrev_map -> Miniml.ml_type -> Miniml.signature
val type_expunge : abbrev_map -> Miniml.ml_type -> Miniml.ml_type
val type_expunge_from_sign : abbrev_map -> Miniml.signature -> Miniml.ml_type -> Miniml.ml_type
val eq_ml_type : Miniml.ml_type -> Miniml.ml_type -> bool
val isTdummy : Miniml.ml_type -> bool
val isMLdummy : Miniml.ml_ast -> bool
val isKill : Miniml.sign -> bool
val anonymous_name : Names.Id.t
val dummy_name : Names.Id.t
val id_of_name : Names.Name.t -> Names.Id.t
val id_of_mlid : Miniml.ml_ident -> Names.Id.t
val collect_lams : Miniml.ml_ast -> Miniml.ml_ident list * Miniml.ml_ast
val collect_n_lams : int -> Miniml.ml_ast -> Miniml.ml_ident list * Miniml.ml_ast
val remove_n_lams : int -> Miniml.ml_ast -> Miniml.ml_ast
val nb_lams : Miniml.ml_ast -> int
val named_lams : Miniml.ml_ident list -> Miniml.ml_ast -> Miniml.ml_ast
val dummy_lams : Miniml.ml_ast -> int -> Miniml.ml_ast
val anonym_or_dummy_lams : Miniml.ml_ast -> Miniml.signature -> Miniml.ml_ast
val eta_args_sign : int -> Miniml.signature -> Miniml.ml_ast list
val ast_map_lift : (int -> Miniml.ml_ast -> Miniml.ml_ast) -> int -> Miniml.ml_ast -> Miniml.ml_ast
val ast_iter : (Miniml.ml_ast -> unit) -> Miniml.ml_ast -> unit
val ast_occurs : int -> Miniml.ml_ast -> bool
val ast_occurs_itvl : int -> int -> Miniml.ml_ast -> bool
val ast_lift : int -> Miniml.ml_ast -> Miniml.ml_ast
val ast_pop : Miniml.ml_ast -> Miniml.ml_ast
val dump_unused_vars : Miniml.ml_ast -> Miniml.ml_ast
val normalize : Miniml.ml_ast -> Miniml.ml_ast
val optimize_fix : Miniml.ml_ast -> Miniml.ml_ast
val inline : Names.GlobRef.t -> Miniml.ml_ast -> bool
val is_basic_pattern : Miniml.ml_pattern -> bool
val has_deep_pattern : Miniml.ml_branch array -> bool
val is_regular_match : Miniml.ml_branch array -> bool
exception Impossible
type sign_kind =
  1. | EmptySig
  2. | NonLogicalSig
  3. | SafeLogicalSig
  4. | UnsafeLogicalSig
val sign_kind : Miniml.signature -> sign_kind
val sign_no_final_keeps : Miniml.signature -> Miniml.signature
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