aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
ModeNameSize
-rw-r--r--clenv.ml18810logplain
-rw-r--r--clenv.mli5331logplain
-rw-r--r--clenvtac.ml4151logplain
-rw-r--r--clenvtac.mli1127logplain
-rw-r--r--doc.tex424logplain
-rw-r--r--evar_refiner.ml2248logplain
-rw-r--r--evar_refiner.mli909logplain
-rw-r--r--goal.ml20975logplain
-rw-r--r--goal.mli9577logplain
-rw-r--r--logic.ml25336logplain
-rw-r--r--logic.mli1833logplain
-rw-r--r--pfedit.ml6057logplain
-rw-r--r--pfedit.mli6190logplain
-rw-r--r--proof.ml15544logplain
-rw-r--r--proof.mli8408logplain
-rw-r--r--proof_global.ml12943logplain
-rw-r--r--proof_global.mli5213logplain
-rw-r--r--proof_type.ml2718logplain
-rw-r--r--proof_type.mli4492logplain
-rw-r--r--proofs.mllib123logplain
-rw-r--r--proofview.ml19822logplain
-rw-r--r--proofview.mli10559logplain
-rw-r--r--redexpr.ml8196logplain
-rw-r--r--redexpr.mli1664logplain
-rw-r--r--refiner.ml14235logplain
-rw-r--r--refiner.mli7364logplain
-rw-r--r--tacmach.ml6945logplain
-rw-r--r--tacmach.mli5689logplain
-rw-r--r--tactic_debug.ml7665logplain
-rw-r--r--tactic_debug.mli2982logplain