package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (6)

Authors

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

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.3.0.tar.gz
sha256=3f0fc283e8644394aa9c7a6e3995b6d9ebbe1e6dda712bf431f9c372dcef95ad

doc/rocq-runtime.tactics/Hints/Hint_db/index.html

Module Hints.Hint_dbSource

Sourcetype t
Sourceval empty : ?name:hint_db_name -> TransparentState.t -> bool -> t
Sourceval map_none : secvars:Names.Id.Pred.t -> t -> FullHint.t list

All hints which have no pattern. * secvars represent the set of section variables that * can be used in the hint.

Sourceval map_all : Environ.env -> secvars:Names.Id.Pred.t -> Names.GlobRef.t -> t -> FullHint.t list

All hints associated to the reference

All hints associated to the reference, respecting modes if evars appear in the arguments and using the discrimination net. Returns a ModeMismatch if there are declared modes and none matches.

Sourceval map_eauto_modes : Environ.env -> Evd.evar_map -> secvars:Names.Id.Pred.t -> (Names.GlobRef.t * EConstr.constr array) -> EConstr.constr -> t -> (mode_restriction NeList.t option * FullHint.t list) option

As map_eauto, but returns the nonempty list of distinct matching mode restrictions in lookup order, including the evars frozen by each restriction. The entire result is None when modes are declared but no mode matches. The first component of the result is None if no modes are declared.

All hints associated to the reference. Precondition: no evars should appear in the arguments, so no modes are checked.

Sourceval remove_one : Environ.env -> Names.GlobRef.t -> t -> t
Sourceval remove_list : Environ.env -> Names.GlobRef.t list -> t -> t
Sourceval iter : (Names.GlobRef.t option -> hint_mode array list -> FullHint.t list -> unit) -> t -> unit
Sourceval fold : (Names.GlobRef.t option -> hint_mode array list -> FullHint.t list -> 'a -> 'a) -> t -> 'a -> 'a
Sourceval use_dn : t -> bool
Sourceval transparent_state : t -> TransparentState.t
Sourceval set_transparent_state : t -> TransparentState.t -> t
Sourceval add_cut : Environ.env -> hints_path -> t -> t
Sourceval cut : t -> hints_path
Sourceval add_modes : Modes.t -> t -> t
Sourceval modes : t -> Modes.t
Sourceval find_mode : Environ.env -> Names.GlobRef.t -> t -> hint_mode array list