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 (3)

Authors

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

Maintainers

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

Sources

rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

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

Module HintsSource

General functions.
Sourceexception Bound
Sourceval decompose_app_bound : Evd.evar_map -> EConstr.constr -> Names.GlobRef.t * EConstr.constr array
Sourcetype debug =
  1. | Debug
  2. | Info
  3. | Off
Sourceval secvars_of_hyps : ('c, 't, 'r) Context.Named.pt -> Names.Id.Pred.t
Sourceval empty_hint_info : 'a Typeclasses.hint_info_gen

Pre-created hint databases

Sourcetype 'a hint_ast =
  1. | Res_pf of 'a
  2. | ERes_pf of 'a
  3. | Give_exact of 'a
  4. | Res_pf_THEN_trivial_fail of 'a
  5. | Unfold_nth of Evaluable.t
  6. | Extern of Pattern.constr_pattern option * Genarg.glob_generic_argument
Sourcetype hint
Sourceval hint_as_term : hint -> UnivGen.sort_context_set option * EConstr.constr
Sourcetype 'a hints_path_atom_gen =
  1. | PathHints of 'a list
  2. | PathAny
Sourcetype hint_db_name = string
Sourcemodule FullHint : sig ... end

The head may not be bound.

Sourcetype hint_mode =
  1. | ModeInput
  2. | ModeNoHeadEvar
  3. | ModeOutput
Sourcetype 'a hints_transparency_target =
  1. | HintsVariables
  2. | HintsConstants
  3. | HintsProjections
  4. | HintsReferences of 'a list
Sourcetype 'a hints_path_gen =
  1. | PathAtom of 'a hints_path_atom_gen
  2. | PathStar of 'a hints_path_gen
  3. | PathSeq of 'a hints_path_gen * 'a hints_path_gen
  4. | PathOr of 'a hints_path_gen * 'a hints_path_gen
  5. | PathEmpty
  6. | PathEpsilon
Sourceval path_matches_epsilon : hints_path -> bool
Sourceval path_derivate : hints_path -> Names.GlobRef.t option -> hints_path
Sourceval pp_hints_path_gen : ('a -> Pp.t) -> 'a hints_path_gen -> Pp.t
Sourceval parse_mode : string -> hint_mode
Sourceval parse_modes : string -> hint_mode list
Sourceval string_of_mode : hint_mode -> string
Sourceval pp_hint_mode : hint_mode -> Pp.t
Sourceval glob_hints_path : pre_hints_path -> hints_path
Sourcetype mode_match =
  1. | NoMode
  2. | WithMode of hint_mode array
Sourcetype 'a with_mode =
  1. | ModeMatch of mode_match * 'a
  2. | ModeMismatch
Sourcemodule Hint_db : sig ... end
Sourcetype hint_db = Hint_db.t
Sourcetype hnf = bool
Sourcetype hint_term
Sourcetype hints_entry =
  1. | HintsResolveEntry of (Typeclasses.hint_info * hnf * hint_term) list
  2. | HintsImmediateEntry of hint_term list
  3. | HintsCutEntry of hints_path
  4. | HintsUnfoldEntry of Evaluable.t list
  5. | HintsTransparencyEntry of Evaluable.t hints_transparency_target * bool
  6. | HintsModeEntry of Names.GlobRef.t * hint_mode list
  7. | HintsExternEntry of Typeclasses.hint_info * Genarg.glob_generic_argument
Sourceval searchtable_map : hint_db_name -> hint_db
Sourceval searchtable_add : (hint_db_name * hint_db) -> unit
Sourcetype hint_locality = Libobject.locality =
  1. | Local
  2. | Export
  3. | SuperGlobal

create_hint_db local name st use_dn. st is a transparency state for unification using this db use_dn switches the use of the discrimination net for all hints and patterns.

Sourceval create_hint_db : bool -> hint_db_name -> TransparentState.t -> bool -> unit
Sourceval remove_hints : locality:hint_locality -> hint_db_name list -> Names.GlobRef.t list -> unit
Sourceval current_db_names : unit -> Util.String.Set.t
Sourceval current_pure_db : unit -> hint_db list
Sourceval add_hints : locality:hint_locality -> hint_db_name list -> hints_entry -> unit
Sourceval hint_globref : Names.GlobRef.t -> hint_term
  • deprecated (8.13) Declare a hint constant instead

A constr which is Hint'ed will be:

  • (1) used as an Exact, if it does not start with a product
  • (2) used as an Apply, if its HNF starts with a product, and has no missing arguments.
  • (3) used as an EApply, if its HNF starts with a product, and has missing arguments.

push_resolve_hyp hname htyp db. used to add an hypothesis to the local hint database; Never raises a user exception; If the hyp cannot be used as a Hint, it is not added.

Sourceval push_resolve_hyp : Environ.env -> Evd.evar_map -> Names.Id.t -> Hint_db.t -> Hint_db.t

Create a Hint database from the pairs (name, constr). Useful to take the current goal hypotheses as hints; Boolean tells if lemmas with evars are allowed

Sourceval make_local_hint_db : Environ.env -> Evd.evar_map -> ?ts:TransparentState.t -> bool -> Tactypes.delayed_open_constr list -> hint_db
Sourceval make_db_list : hint_db_name list -> hint_db list
Sourceval wrap_hint_warning : 'a Proofview.tactic -> 'a Proofview.tactic

Use around toplevel calls to hint-using tactics, to enable the tracking of non-imported hints. Any tactic calling run_hint must be wrapped this way.

Sourceval wrap_hint_warning_fun : Environ.env -> Evd.evar_map -> (Evd.evar_map -> 'a * Evd.evar_map) -> 'a * Evd.evar_map

Variant of the above for non-tactics

Sourceval hint_res_pf : ?with_evars:bool -> ?with_classes:bool -> ?flags:Unification.unify_flags -> hint -> unit Proofview.tactic

Printing hints

Sourceval pr_searchtable : Environ.env -> Evd.evar_map -> Pp.t
Sourceval pr_applicable_hint : Proof.t -> Pp.t
Sourceval pr_hint_db_by_name : Environ.env -> Evd.evar_map -> hint_db_name -> Pp.t
Sourceval pr_hint_db_env : Environ.env -> Evd.evar_map -> Hint_db.t -> Pp.t