Individual skill

coq

Develops and checks proofs in Coq and its renamed successor Rocq, covering the `_CoqProject` and `coq_makefile` (or `rocq makefile`) build, `coqc` and `coqchk` (or `rocq compile` and `rocq check`), finding lemmas with `Search` and `SearchPattern`, choosing `Qed` versus `Defined` and `Opaque` versus `Transparent`, finishing without `Admitted`, auditing with `Print Assumptions`, and stating the exact proposition the informal claim makes. Use when asked to prove, formalize, check or repair a Coq or Rocq development; use lean4-mathlib for Lean, and ordinary mathematical writing for informal proofs.

backend/cli/skills/other/coq/SKILL.md

Read pinned source

Source commit a08e0ad0ad3d6448123039ee4659163eb2e35d99

What was checked

Matches the observed repository HEAD: Yes
Scanner rules are current: Yes
Repository scan complete: No
Skill scan complete: Yes
Observed behavior: Network or broad shell
Last checked: Nov 2, 2026

These are observations at the recorded commit, not a guarantee of safety. Review the source before running it.

Install this skill

Choose an agent in your Stack or copy a command below. Commands fetch the pinned commit and copy only this skill directory. Existing destinations are refused. Copying a command does not install anything.

An install command is unavailable: current rules, complete repository and skill scans, an eligible behavior level and a permitted license are required.

Repository context

Repository stars (not skill ratings): 4,353
Repository last updated: Nov 6, 2026
License: Apache-2.0

Observed agent integration: No specific integration evidence. Standard SKILL.md installation does not imply verified compatibility.

agent Repository topic
ai Repository topic
bun Repository topic
cli Repository topic
llm Repository topic
ml Repository topic
open-source Repository topic
research Repository topic
science Repository topic
ai-agent Repository topic
writing Derived category

Files and excerpt

File metadata and permitted, redacted excerpts come from the recorded scan. Source links are pinned to that commit.

Browse files

SKILL.mdcore · 6,525 bytes

Read excerpt


# Coq and Rocq

`Admitted` compiles, and so does a theorem about the wrong proposition. The kernel checks
the proof; you check that the statement is the claim, that no assumption was smuggled in,
and that the compiled library passes an independent check. Coq 8.x commands and the Rocq 9
`rocq` subcommands are both given; use the pair the installed version provides.

## Project

1. `_CoqProject` lists the logical mapping and the files: `-Q theories MyLib` (or `-R`
   for recursive legacy mapping), optional `-arg -w -arg -notation-overridden`, then one
   `.v` path per line. Generate the Makefile with `coq_makefile -f _CoqProject -o Makefile`
   (Rocq 9: `rocq makefile -f _CoqProject -o Makefile`) and build with `make`. A single
   file compiles with `coqc -Q theories MyLib theories/File.v` (`rocq compile`). Dune