package rocq-runtime
The Rocq Prover -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
doc/ltac_plugin/Ltac_plugin/Tacintern/index.html
Module Ltac_plugin.Tacintern
Source
Globalization of tactic expressions : Conversion from raw_tactic_expr
to glob_tactic_expr
Source
type glob_sign = Genintern.glob_sign = {
ltacvars : Names.Id.Set.t;
genv : Environ.env;
extra : Genintern.Store.t;
intern_sign : Genintern.intern_variable_status;
strict_check : bool;
}
build an empty glob_sign
using Global.env()
as environment; strict_check if true
Main globalization functions
Source
val glob_tactic_env :
Names.Id.t list ->
Environ.env ->
Tacexpr.raw_tactic_expr ->
Tacexpr.glob_tactic_expr
Low-level variants
Source
val intern_tactic_or_tacarg :
glob_sign ->
Tacexpr.raw_tactic_expr ->
Tacexpr.glob_tactic_expr
Source
val intern_constr_with_bindings :
glob_sign ->
(Constrexpr.constr_expr * Constrexpr.constr_expr Tactypes.bindings) ->
Genintern.glob_constr_and_expr
* Genintern.glob_constr_and_expr Tactypes.bindings
Adds a globalization function for extra generic arguments
Reduction expressions
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>