package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

Module `Ltac2_plugin.Tac2extravals`Source

This module declares the parsing, intern and interp functions for various builtin expressions (constr quotations, syntactic classses, etc)