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/rocq-runtime.tactics/Redexpr/Intern/index.html
Module Redexpr.InternSource
Source
type ('constr, 'ref, 'pat) intern_env = {strict_check : bool;local_ref : Libnames.qualid -> 'ref option;global_ref : ?short:Names.lident -> Evaluable.t -> 'ref;intern_constr : Constrexpr.constr_expr -> 'constr;ltac_sign : Constrintern.ltac_sign;intern_pattern : Constrexpr.constr_expr -> 'pat;pattern_of_glob : Glob_term.glob_constr -> 'pat;
}Source
val intern_red_expr :
('a, 'b, 'c) intern_env ->
Genredexpr.raw_red_expr ->
('a, 'b, 'c, int Locus.or_var) Genredexpr.red_expr_genSource
val from_env :
Environ.env ->
(Glob_term.glob_constr, Evaluable.t, Glob_term.glob_constr) intern_env