aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
ModeNameSize
-rw-r--r--clenv.ml18859logplain
-rw-r--r--clenv.mli5331logplain
-rw-r--r--clenvtac.ml4053logplain
-rw-r--r--clenvtac.mli1127logplain
-rw-r--r--doc.tex424logplain
-rw-r--r--evar_refiner.ml2316logplain
-rw-r--r--evar_refiner.mli909logplain
-rw-r--r--goal.ml21239logplain
-rw-r--r--goal.mli9454logplain
-rw-r--r--logic.ml25321logplain
-rw-r--r--logic.mli1739logplain
-rw-r--r--monads.ml7285logplain
-rw-r--r--pfedit.ml6071logplain
-rw-r--r--pfedit.mli6126logplain
-rw-r--r--proof.ml15333logplain
-rw-r--r--proof.mli8341logplain
-rw-r--r--proof_global.ml13079logplain
-rw-r--r--proof_global.mli5224logplain
-rw-r--r--proof_type.ml1798logplain
-rw-r--r--proof_type.mli3280logplain
-rw-r--r--proofs.mllib130logplain
-rw-r--r--proofview.ml18729logplain
-rw-r--r--proofview.mli10589logplain
-rw-r--r--redexpr.ml8850logplain
-rw-r--r--redexpr.mli1664logplain
-rw-r--r--refiner.ml13822logplain
-rw-r--r--refiner.mli6792logplain
-rw-r--r--tacmach.ml6699logplain
-rw-r--r--tacmach.mli5426logplain
-rw-r--r--tactic_debug.ml7503logplain
-rw-r--r--tactic_debug.mli2974logplain