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.18.0.tar.gz
md5=8d852367b54f095d9fbabd000304d450
sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50

doc/micromega_plugin/Micromega_plugin/Mutils/index.html

Module Micromega_plugin.MutilsSource

Sourcemodule Int : sig ... end
Sourcemodule ISet : sig ... end
Sourcemodule IMap : sig ... end
Sourcemodule Cmp : sig ... end
Sourcemodule Tag : sig ... end
Sourcemodule TagSet : CSig.SetS with type elt = Tag.t
Sourcemodule McPrinter : sig ... end
Sourceval pp_list : string -> (Stdlib.out_channel -> 'a -> unit) -> Stdlib.out_channel -> 'a list -> unit
Sourcemodule CamlToCoq : sig ... end
Sourcemodule CoqToCaml : sig ... end
Sourcemodule Hash : sig ... end
Sourceval all_pairs : ('a -> 'a -> 'b) -> 'a list -> 'b list
Sourceval try_any : (('a -> 'b option) * 'c) list -> 'a -> 'b option
Sourceval is_sublist : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
Sourceval extract : ('a -> 'b option) -> 'a list -> ('b * 'a) option * 'a list
Sourceval extract_all : ('a -> 'b option) -> 'a list -> 'b list * 'a list
Sourceval extract_best : ('a -> 'b option) -> ('b -> 'b -> bool) -> 'a list -> ('b * 'a) option * 'a list
Sourceval find_some : ('a -> 'b option) -> 'a list -> 'b option
Sourceval iterate_until_stable : ('a -> 'a option) -> 'a -> 'a
Sourceval simplify : ('a -> 'a option) -> 'a list -> 'a list option
Sourceval saturate : ('a -> 'b option) -> (('b * 'a) -> 'a -> 'a option) -> 'a list -> 'a list
Sourceval saturate_bin : (module Stdlib.Set.S with type elt = 'a) -> ('a -> 'a -> 'a option) -> 'a list -> 'a list
Sourceval generate : ('a -> 'b option) -> 'a list -> 'b list
Sourceval app_funs : ('a -> 'b option) list -> 'a -> 'b option
Sourceval command : string -> string array -> 'a -> 'b