Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package coq-waterproof
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
Interface to load and unload usual hint databases such as reals, integers, classical logic, ...
Type referencing all database lists that a hint_dataset should contain
val database_type_of_string : string -> database_typeConverts a string to a database_type
val name : hint_dataset -> stringReturns the name of the given dataset
val get_databases : hint_dataset -> database_type -> Hints.hint_db_name listReturns the list of databases for the given database_type
val new_dataset : string -> hint_datasetCreate a new empty dataset with a given name
val set_databases :
hint_dataset ->
database_type ->
string list ->
hint_datasetSets the databases of the given type for the given dataset
val empty : hint_datasetval core : hint_datasetval algebra : hint_datasetval integers : hint_datasetval reals_and_integers : hint_datasetval sets : hint_datasetval intuition : hint_datasetval classical_epsilon : hint_dataset