package coq-core

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

Install 

dune-project
 Dependency

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

Authors

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

Maintainers

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

Sources

coq-8.20.1.tar.gz
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2

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