package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

Module `Ltac2_plugin.Tac2subst`Source

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