package coq-waterproof

  1. Overview
  2. Docs

Module Waterproof.Unfold_frameworkSource

In this module we keep two tables:

  • wp_unfold_map a map from strings to global references, that is used to keep track of the introduced notations, and the global reference they are associated with
  • wp_unfold_tbl a table from global references to unfold actions, that can later be used by the unfold framework. The unfold actions can be of three types:
  • unfold the definition associated to the global reference
  • apply a bi-implication
  • rewrite an equality
Sourcetype unfold_action =
  1. | Unfold of string * Names.GlobRef.t
  2. | Apply of string * EConstr.constr
  3. | Rewrite of string * EConstr.constr

A type to represent the different unfold actions, and the data they need.

Sourcetype unfold_entry =
  1. | Unfold_entry of string
  2. | Apply_entry of string * Constrexpr.constr_expr
  3. | Rewrite_entry of string * Constrexpr.constr_expr

A type that represents the datastructure that can be added to the unfold table. When it is added, it will be converted to an unfold action.

Sourcemodule StringMap : Map.S with type key = string
Sourceval wp_unfold_map : Names.GlobRef.t StringMap.t ref
Sourceval add_to_unfold_map : string list -> Names.GlobRef.t -> unit
Sourceval register_unfold : string list -> Libnames.qualid -> Ltac2_plugin.Tac2entries.notation_interpretation_data * Ltac2_plugin.Tac2entries.notation_interpretation_data
Sourceval register_unfold_entry : Names.GlobRef.t -> unfold_entry -> unit
Sourceval extract_def : string -> Names.GlobRef.t option
Sourceval wp_unfold_tbl : (Names.GlobRef.t, unfold_action) Hashtbl.t ref
Sourceval find_unfold_actions_by_ref : Names.GlobRef.t -> unfold_action list
Sourceval find_unfold_actions_by_str : string -> unfold_action list
Sourceval get_all_references : unit -> Names.GlobRef.t list