summaryrefslogtreecommitdiff
path: root/test-suite/success
ModeNameSize
-rw-r--r--Abstract.v446logplain
-rw-r--r--Case1.v335logplain
-rw-r--r--Case10.v738logplain
-rw-r--r--Case11.v341logplain
-rw-r--r--Case12.v2074logplain
-rw-r--r--Case13.v1725logplain
-rw-r--r--Case14.v510logplain
-rw-r--r--Case15.v1318logplain
-rw-r--r--Case16.v405logplain
-rw-r--r--Case17.v1850logplain
-rw-r--r--Case18.v214logplain
-rw-r--r--Case2.v306logplain
-rw-r--r--Case5.v365logplain
-rw-r--r--Case6.v583logplain
-rw-r--r--Case7.v474logplain
-rw-r--r--Case8.v338logplain
-rw-r--r--Case9.v2237logplain
-rw-r--r--CaseAlias.v386logplain
-rw-r--r--Cases.v38183logplain
-rw-r--r--CasesDep.v10927logplain
-rw-r--r--Check.v795logplain
-rw-r--r--Conjecture.v231logplain
-rw-r--r--DHyp.v1logplain
-rw-r--r--Decompose.v218logplain
-rw-r--r--DiscrR.v435logplain
-rw-r--r--Discriminate.v206logplain
-rw-r--r--Field.v1699logplain
-rw-r--r--Fixpoint.v981logplain
-rw-r--r--Fourier.v283logplain
-rw-r--r--Funind.v8846logplain
-rw-r--r--Generalize.v176logplain
-rw-r--r--Hints.v1261logplain
-rw-r--r--ImplicitTactic.v549logplain
-rw-r--r--Inductive.v1427logplain
-rw-r--r--Injection.v928logplain
-rw-r--r--Inversion.v2676logplain
-rw-r--r--LetIn.v356logplain
-rw-r--r--MatchFail.v822logplain
-rw-r--r--Mod_ltac.v302logplain
-rw-r--r--Mod_params.v1445logplain
-rw-r--r--Mod_strengthen.v963logplain
-rw-r--r--Mod_type.v269logplain
-rw-r--r--NatRing.v133logplain
-rw-r--r--Notations.v286logplain
-rw-r--r--Omega.v2201logplain
-rw-r--r--Omega0.v2467logplain
-rw-r--r--Omega2.v764logplain
-rw-r--r--PPFix.v207logplain
-rw-r--r--Print.v282logplain
-rw-r--r--Projection.v1154logplain
-rw-r--r--ROmega.v2356logplain
-rw-r--r--ROmega0.v2533logplain
-rw-r--r--ROmega2.v775logplain
-rw-r--r--RecTutorial.v25255logplain
-rw-r--r--Record.v106logplain
-rw-r--r--Reg.v3094logplain
-rw-r--r--Remark.v172logplain
-rw-r--r--Rename.v220logplain
-rw-r--r--Require.v88logplain
-rw-r--r--Reset.v77logplain
-rw-r--r--Scopes.v157logplain
-rw-r--r--Simplify_eq.v258logplain
-rw-r--r--Tauto.v5202logplain
-rw-r--r--TestRefine.v4406logplain
-rw-r--r--Try.v182logplain
-rw-r--r--autorewritein.v527logplain
-rw-r--r--cc.v1759logplain
-rw-r--r--coercions.v724logplain
-rw-r--r--coqbugs0181.v211logplain
-rw-r--r--destruct.v489logplain
-rw-r--r--eauto.v1868logplain
-rw-r--r--eqdecide.v912logplain
-rw-r--r--evars.v1991logplain
-rw-r--r--extraction.v112logplain
-rw-r--r--fix.v1732logplain
-rw-r--r--if.v366logplain
-rw-r--r--implicit.v786logplain
-rw-r--r--import_lib.v3467logplain
-rw-r--r--import_mod.v993logplain
-rw-r--r--inds_type_sec.v594logplain
-rw-r--r--induct.v698logplain
-rw-r--r--intros.v168logplain
-rw-r--r--ltac.v3151logplain
-rw-r--r--mutual_ind.v1604logplain
-rw-r--r--options.v686logplain
-rw-r--r--params_ind.v93logplain
-rw-r--r--refine.v1939logplain
-rw-r--r--rewrite.v530logplain
-rw-r--r--set.v90logplain
-rw-r--r--setoid_test.v1953logplain
-rw-r--r--setoid_test2.v8151logplain
-rw-r--r--setoid_test_function_space.v1387logplain
-rw-r--r--simpl.v655logplain
-rw-r--r--unfold.v644logplain
-rw-r--r--unicode_utf8.v372logplain
-rw-r--r--univers.v1646logplain