package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

coq.inria.fr Readme Edit opam file Versions (9)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b

doc/extraction_plugin/Extraction_plugin/Mlutil/index.html

Module Extraction_plugin.MlutilSource

Sourceval reset_meta_count : unit -> unit
Sourceval new_meta : 'a -> Miniml.ml_type
Sourceval type_subst_list : Miniml.ml_type list -> Miniml.ml_type -> Miniml.ml_type
Sourceval type_subst_vect : Miniml.ml_type array -> Miniml.ml_type -> Miniml.ml_type
Sourceval instantiation : Miniml.ml_schema -> Miniml.ml_type
Sourceval needs_magic : (Miniml.ml_type * Miniml.ml_type) -> bool
Sourceval put_magic_if : bool -> Miniml.ml_ast -> Miniml.ml_ast
Sourceval generalizable : Miniml.ml_ast -> bool
Sourcemodule Mlenv : sig ... end
Sourceval type_mem_kn : Names.MutInd.t -> Miniml.ml_type -> bool
Sourceval type_maxvar : Miniml.ml_type -> int
Sourceval type_recomp : (Miniml.ml_type list * Miniml.ml_type) -> Miniml.ml_type
Sourcetype abbrev_map = Names.GlobRef.t -> Miniml.ml_type option
Sourceval type_to_signature : abbrev_map -> Miniml.ml_type -> Miniml.signature
Sourceval type_expunge_from_sign : abbrev_map -> Miniml.signature -> Miniml.ml_type -> Miniml.ml_type
Sourceval eq_ml_type : Miniml.ml_type -> Miniml.ml_type -> bool
Sourceval isTdummy : Miniml.ml_type -> bool
Sourceval isMLdummy : Miniml.ml_ast -> bool
Sourceval isKill : Miniml.sign -> bool
Sourceval anonymous_name : Names.Id.t
Sourceval dummy_name : Names.Id.t
Sourceval id_of_name : Names.Name.t -> Names.Id.t
Sourceval id_of_mlid : Miniml.ml_ident -> Names.Id.t
Sourceval collect_n_lams : int -> Miniml.ml_ast -> Miniml.ml_ident list * Miniml.ml_ast
Sourceval remove_n_lams : int -> Miniml.ml_ast -> Miniml.ml_ast
Sourceval nb_lams : Miniml.ml_ast -> int
Sourceval dummy_lams : Miniml.ml_ast -> int -> Miniml.ml_ast
Sourceval anonym_or_dummy_lams : Miniml.ml_ast -> Miniml.signature -> Miniml.ml_ast
Sourceval eta_args_sign : int -> Miniml.signature -> Miniml.ml_ast list
Sourceval ast_map_lift : (int -> Miniml.ml_ast -> Miniml.ml_ast) -> int -> Miniml.ml_ast -> Miniml.ml_ast
Sourceval ast_iter : (Miniml.ml_ast -> unit) -> Miniml.ml_ast -> unit
Sourceval ast_occurs : int -> Miniml.ml_ast -> bool
Sourceval ast_occurs_itvl : int -> int -> Miniml.ml_ast -> bool
Sourceval ast_lift : int -> Miniml.ml_ast -> Miniml.ml_ast
Sourceval dump_unused_vars : Miniml.ml_ast -> Miniml.ml_ast
Sourceval optimize_fix : Miniml.ml_ast -> Miniml.ml_ast
Sourceval inline : Names.GlobRef.t -> Miniml.ml_ast -> bool
Sourceval is_basic_pattern : Miniml.ml_pattern -> bool
Sourceval has_deep_pattern : Miniml.ml_branch array -> bool
Sourceval is_regular_match : Miniml.ml_branch array -> bool
Sourceexception Impossible
Sourcetype sign_kind =
  1. | EmptySig
  2. | NonLogicalSig
  3. | SafeLogicalSig
  4. | UnsafeLogicalSig
Sourceval 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