package rocq-runtime

  1. Overview
  2. Docs
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.TacinternSource

Globalization of tactic expressions : Conversion from raw_tactic_expr to glob_tactic_expr

Sourcetype glob_sign = Genintern.glob_sign = {
  1. ltacvars : Names.Id.Set.t;
  2. genv : Environ.env;
  3. extra : Genintern.Store.t;
  4. intern_sign : Genintern.intern_variable_status;
  5. strict_check : bool;
}
Sourceval make_empty_glob_sign : strict:bool -> glob_sign

build an empty glob_sign using Global.env() as environment; strict_check if true

Main globalization functions

Low-level variants

Adds a globalization function for extra generic arguments

Reduction expressions

OCaml

Innovation. Community. Security.