package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install

dune-project
 Dependency

Authors

Maintainers

Sources

rocq-9.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

doc/src/ltac2_ltac1_plugin/tac2quote_ltac1.ml.html

Source file tac2quote_ltac1.ml

1
2
3
4
open Ltac2_plugin.Tac2dyn

let wit_ltac1 = Arg.create "ltac1"
let wit_ltac1val = Arg.create "ltac1val"