package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

dune-project

Dependency

sha256=3f0fc283e8644394aa9c7a6e3995b6d9ebbe1e6dda712bf431f9c372dcef95ad

val subst_type : 
  Mod_subst.substitution ->
  'a Tac2expr.glb_typexpr ->
  'a Tac2expr.glb_typexpr

val subst_expr : 
  Mod_subst.substitution ->
  Tac2expr.glb_tacexpr ->
  Tac2expr.glb_tacexpr

val subst_quant_typedef : 
  Mod_subst.substitution ->
  Tac2expr.glb_quant_typedef ->
  Tac2expr.glb_quant_typedef

val subst_type_scheme : 
  Mod_subst.substitution ->
  Tac2expr.type_scheme ->
  Tac2expr.type_scheme

val subst_rawexpr : 
  Mod_subst.substitution ->
  Tac2expr.raw_tacexpr ->
  Tac2expr.raw_tacexpr