University of California, San Diego
PeaCoq is a web-based front-end to the Coq proof assistant.
It provides an interface similar to CoqIDE or ProofGeneral, but additionally offers a proof mode called "Proof Tree" with the following features:
- preview of the outcome of running a tactic
- visual diff of the context before and after a tactic
- context clutter reduction using browser overlay
View on Github