aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
ModeNameSize
-rw-r--r--clenv.ml18414logplain
-rw-r--r--clenv.mli4221logplain
-rw-r--r--clenvtac.ml4442logplain
-rw-r--r--clenvtac.mli1238logplain
-rw-r--r--doc.tex424logplain
-rw-r--r--evar_refiner.ml2554logplain
-rw-r--r--evar_refiner.mli909logplain
-rw-r--r--goal.ml21927logplain
-rw-r--r--goal.mli9837logplain
-rw-r--r--logic.ml25694logplain
-rw-r--r--logic.mli1742logplain
-rw-r--r--monads.ml6978logplain
-rw-r--r--pfedit.ml5740logplain
-rw-r--r--pfedit.mli5902logplain
-rw-r--r--proof.ml10240logplain
-rw-r--r--proof.mli6938logplain
-rw-r--r--proof_global.ml13816logplain
-rw-r--r--proof_global.mli5661logplain
-rw-r--r--proof_type.ml1790logplain
-rw-r--r--proof_type.mli3220logplain
-rw-r--r--proofs.mllib130logplain
-rw-r--r--proofview.ml21679logplain
-rw-r--r--proofview.mli12321logplain
-rw-r--r--redexpr.ml8607logplain
-rw-r--r--redexpr.mli1682logplain
-rw-r--r--refiner.ml13452logplain
-rw-r--r--refiner.mli6944logplain
-rw-r--r--tacmach.ml8022logplain
-rw-r--r--tacmach.mli6080logplain
-rw-r--r--tactic_debug.ml7412logplain
-rw-r--r--tactic_debug.mli2957logplain