package coq-waterproof

  1. Overview
  2. Docs
val loaded_hint_dataset : string list ref

Contains the hint dataset that is currently loaded

Dictionary with dataset names as keys and datasets as values

val load_dataset : string -> unit

Replace all current loaded hints by the ones declared in the hint_dataset

val remove_dataset : string -> unit

Removes a dataset to the currently loaded hint datasets

val clear_dataset : unit -> unit

Clears all the currently loaded datasets

val create_new_dataset : string -> unit

Creates a new empty dataset from a given name

val populate_dataset : string -> Hint_dataset_declarations.database_type -> string list -> unit

Sets the databases of a given database_type in a given dataset

Returns the list of databases of the current loaded dataset for the given Hint_dataset_declarations.database_type

OCaml

Innovation. Community. Security.