aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
ModeNameSize
-rw-r--r--clenv.ml18810logplain
-rw-r--r--clenv.mli5353logplain
-rw-r--r--clenvtac.ml4138logplain
-rw-r--r--clenvtac.mli1149logplain
-rw-r--r--doc.tex424logplain
-rw-r--r--evar_refiner.ml2249logplain
-rw-r--r--evar_refiner.mli908logplain
-rw-r--r--goal.ml20989logplain
-rw-r--r--goal.mli9561logplain
-rw-r--r--logic.ml25332logplain
-rw-r--r--logic.mli1833logplain
-rw-r--r--pfedit.ml6000logplain
-rw-r--r--pfedit.mli6202logplain
-rw-r--r--proof.ml15124logplain
-rw-r--r--proof.mli7913logplain
-rw-r--r--proof_global.ml12943logplain
-rw-r--r--proof_global.mli5212logplain
-rw-r--r--proof_type.ml2699logplain
-rw-r--r--proof_type.mli4473logplain
-rw-r--r--proofs.mllib130logplain
-rw-r--r--proofview.ml19737logplain
-rw-r--r--proofview.mli9716logplain
-rw-r--r--redexpr.ml8191logplain
-rw-r--r--redexpr.mli1663logplain
-rw-r--r--refiner.ml14235logplain
-rw-r--r--refiner.mli7364logplain
-rw-r--r--tacmach.ml6945logplain
-rw-r--r--tacmach.mli5674logplain
-rw-r--r--tacops.ml1696logplain
-rw-r--r--tacops.mli741logplain
-rw-r--r--tactic_debug.ml7505logplain
-rw-r--r--tactic_debug.mli2980logplain