summaryrefslogtreecommitdiff
path: root/test-suite/success
ModeNameSize
-rw-r--r--Abstract.v8445logplain
-rw-r--r--Case1.v400logplain
-rw-r--r--Case10.v764logplain
-rw-r--r--Case11.v285logplain
-rw-r--r--Case12.v1442logplain
-rw-r--r--Case13.v959logplain
-rw-r--r--Case14.v489logplain
-rw-r--r--Case15.v1303logplain
-rw-r--r--Case16.v388logplain
-rw-r--r--Case17.v1893logplain
-rw-r--r--Case2.v339logplain
-rw-r--r--Case5.v351logplain
-rw-r--r--Case6.v597logplain
-rw-r--r--Case7.v459logplain
-rw-r--r--Case9.v2270logplain
-rw-r--r--CaseAlias.v380logplain
-rw-r--r--Cases.v46156logplain
-rw-r--r--CasesDep.v10886logplain
-rw-r--r--Check.v795logplain
-rw-r--r--Conjecture.v210logplain
-rw-r--r--DHyp.v217logplain
-rw-r--r--Decompose.v187logplain
-rw-r--r--Destruct.v236logplain
-rw-r--r--DiscrR.v395logplain
-rw-r--r--Discriminate.v196logplain
-rw-r--r--Field.v1498logplain
-rw-r--r--Fourier.v300logplain
-rw-r--r--Funind.v9863logplain
-rw-r--r--Generalize.v137logplain
-rw-r--r--Hints.v1559logplain
-rw-r--r--Inductive.v1057logplain
-rw-r--r--Injection.v814logplain
-rw-r--r--Inversion.v2319logplain
-rw-r--r--LetIn.v314logplain
-rw-r--r--MatchFail.v958logplain
-rw-r--r--Mod_ltac.v264logplain
-rw-r--r--Mod_params.v1325logplain
-rw-r--r--Mod_strengthen.v889logplain
-rw-r--r--NatRing.v144logplain
-rw-r--r--Omega.v1702logplain
-rw-r--r--PPFix.v8206logplain
-rw-r--r--Print.v297logplain
-rw-r--r--Projection.v1059logplain
-rw-r--r--Record.v105logplain
-rw-r--r--Reg.v2837logplain
-rw-r--r--Remark.v172logplain
-rw-r--r--Rename.v78logplain
-rw-r--r--Require.v85logplain
-rw-r--r--Scopes.v157logplain
-rw-r--r--Simplify_eq.v241logplain
-rw-r--r--Tauto.v4831logplain
-rw-r--r--Try.v176logplain
-rw-r--r--cc.v1721logplain
-rw-r--r--coercions.v202logplain
-rw-r--r--coqbugs0181.v202logplain
-rw-r--r--eauto.v1706logplain
-rw-r--r--eqdecide.v838logplain
-rw-r--r--evars.v802logplain
-rw-r--r--fix.v1661logplain
-rw-r--r--if.v154logplain
-rw-r--r--implicit.v741logplain
-rw-r--r--import_lib.v3550logplain
-rw-r--r--import_mod.v981logplain
-rw-r--r--inds_type_sec.v590logplain
-rw-r--r--induct.v693logplain
-rw-r--r--ltac.v1744logplain
-rw-r--r--mutual_ind.v1515logplain
-rw-r--r--options.v662logplain
-rw-r--r--refine.v498logplain
-rw-r--r--setoid_test.v1708logplain
-rw-r--r--unfold.v648logplain
-rw-r--r--univers.v305logplain