proofs.mllib « proofs - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

path: root/proofs/proofs.mllib

blob: 05b86b1a04eeb5bf5fe9992f091df2fcfb3521e5 (plain)

Tacexpr
Proof_type
Redexpr
Proof_trees
Logic
Refiner
Evar_refiner
Tacmach
Pfedit
Tactic_debug
Clenvtac
Decl_mode