summaryrefslogtreecommitdiff
path: root/proofs
ModeNameSize
-rw-r--r--clenv.ml18780logplain
-rw-r--r--clenv.mli5326logplain
-rw-r--r--clenvtac.ml4171logplain
-rw-r--r--clenvtac.mli1137logplain
-rw-r--r--doc.tex424logplain
-rw-r--r--evar_refiner.ml2267logplain
-rw-r--r--evar_refiner.mli908logplain
-rw-r--r--goal.ml21532logplain
-rw-r--r--goal.mli9567logplain
-rw-r--r--logic.ml25351logplain
-rw-r--r--logic.mli1833logplain
-rw-r--r--pfedit.ml6103logplain
-rw-r--r--pfedit.mli6175logplain
-rw-r--r--proof.ml15568logplain
-rw-r--r--proof.mli8437logplain
-rw-r--r--proof_global.ml12972logplain
-rw-r--r--proof_global.mli5199logplain
-rw-r--r--proof_type.ml2701logplain
-rw-r--r--proof_type.mli4475logplain
-rw-r--r--proofs.mllib131logplain
-rw-r--r--proofview.ml19753logplain
-rw-r--r--proofview.mli10586logplain
-rw-r--r--redexpr.ml7958logplain
-rw-r--r--redexpr.mli1652logplain
-rw-r--r--refiner.ml14313logplain
-rw-r--r--refiner.mli7364logplain
-rw-r--r--tacexpr.ml12975logplain
-rw-r--r--tacmach.ml6936logplain
-rw-r--r--tacmach.mli5671logplain
-rw-r--r--tactic_debug.ml7529logplain
-rw-r--r--tactic_debug.mli2982logplain