package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

locate_global_with_alias locates global reference possibly following a notation if this notation has a role of aliasing; raise Not_found if not bound in the global env; raise a UserError if bound to a syntactic def that does not denote a reference

val locate_global_with_alias : ?head:bool -> Libnames.qualid -> Names.GlobRef.t
val global_of_extended_global : Globnames.extended_global_reference -> Names.GlobRef.t option

Extract a global_reference from a reference that can be an "alias". If the reference points to a more complex term, we return None

val global_with_alias : ?head:bool -> Libnames.qualid -> Names.GlobRef.t

Locate a reference taking into account possible "alias" notations. May raise Nametab.GlobalizationError _ for an unknown reference, or a UserError if bound to a syntactic def that does not denote a reference.

val global_constant_with_alias : Libnames.qualid -> Names.Constant.t

The same for constants

val global_inductive_with_alias : Libnames.qualid -> Names.inductive

The same for inductive types

val global_constructor_with_alias : Libnames.qualid -> Names.constructor

The same for constructors of an inductive type

val smart_global : ?head:bool -> Libnames.qualid Constrexpr.or_by_notation -> Names.GlobRef.t

Locate a reference taking into account notations and "aliases"

The same for constants

The same for inductive types

The same for constructors of an inductive type

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct