package coq-core

You can search for identifiers within the package.

in-package search v0.2.0

The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

coq.inria.fr Readme Edit opam file Versions (9)

Authors

T

The Coq development team, INRIA, CNRS, and contributors

Maintainers

T

The Coq development team <coqdev@inria.fr>

Sources

coq-8.19.0.tar.gz

md5=64b49dbc3205477bd7517642c0b9cbb6

sha512=02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b

doc/coq-core.interp/Smartlocate/index.html

Module `Smartlocate`Source

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

Sourceval locate_global_with_alias : ?head:bool -> Libnames.qualid -> Names.GlobRef.t

Source

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

Sourceval 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.

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

The same for constants

Sourceval global_inductive_with_alias : Libnames.qualid -> Names.inductive

The same for inductive types

Sourceval global_constructor_with_alias : Libnames.qualid -> Names.constructor

The same for constructors of an inductive type

Source

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

Locate a reference taking into account notations and "aliases"

Source

val smart_global_constant : 
  Libnames.qualid Constrexpr.or_by_notation ->
  Names.Constant.t

The same for constants

Source

val smart_global_inductive : 
  Libnames.qualid Constrexpr.or_by_notation ->
  Names.inductive

The same for inductive types

Source

val smart_global_constructor : 
  Libnames.qualid Constrexpr.or_by_notation ->
  Names.constructor

The same for constructors of an inductive type

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.interp/Smartlocate/index.html

Module SmartlocateSource

Module `Smartlocate`Source