aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
ModeNameSize
-rw-r--r--Abstract.v445logplain
-rw-r--r--AdvancedCanonicalStructure.v2844logplain
-rw-r--r--AdvancedTypeClasses.v2253logplain
-rw-r--r--CanonicalStructure.v713logplain
-rw-r--r--Case1.v335logplain
-rw-r--r--Case10.v738logplain
-rw-r--r--Case11.v349logplain
-rw-r--r--Case12.v2083logplain
-rw-r--r--Case13.v2149logplain
-rw-r--r--Case14.v510logplain
-rw-r--r--Case15.v1315logplain
-rw-r--r--Case16.v409logplain
-rw-r--r--Case17.v1860logplain
-rw-r--r--Case18.v513logplain
-rw-r--r--Case19.v542logplain
-rw-r--r--Case2.v306logplain
-rw-r--r--Case20.v1106logplain
-rw-r--r--Case3.v720logplain
-rw-r--r--Case5.v365logplain
-rw-r--r--Case6.v583logplain
-rw-r--r--Case7.v478logplain
-rw-r--r--Case8.v338logplain
-rw-r--r--Case9.v2269logplain
-rw-r--r--CaseAlias.v2598logplain
-rw-r--r--CaseInClause.v659logplain
-rw-r--r--Cases-bug1834.v383logplain
-rw-r--r--Cases.v39094logplain
-rw-r--r--CasesDep.v14537logplain
-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.v644logplain
-rw-r--r--Field.v1978logplain
-rw-r--r--Fixpoint.v2347logplain
-rw-r--r--Fourier.v281logplain
-rw-r--r--Funind.v10039logplain
-rw-r--r--Generalization.v282logplain
-rw-r--r--Generalize.v176logplain
-rw-r--r--Hints.v1577logplain
-rw-r--r--ImplicitArguments.v627logplain
-rw-r--r--ImplicitTactic.v549logplain
-rw-r--r--Import.v218logplain
-rw-r--r--Inductive.v3408logplain
-rw-r--r--Injection.v2175logplain
-rw-r--r--Inversion.v3709logplain
-rw-r--r--LetIn.v356logplain
-rw-r--r--LetPat.v1760logplain
-rw-r--r--MatchFail.v836logplain
-rw-r--r--Mod_ltac.v302logplain
-rw-r--r--Mod_params.v1375logplain
-rw-r--r--Mod_strengthen.v963logplain
-rw-r--r--Mod_type.v519logplain
-rw-r--r--NatRing.v125logplain
-rw-r--r--Notations.v3155logplain
-rw-r--r--Nsatz.v14259logplain
-rw-r--r--NumberScopes.v1368logplain
-rw-r--r--Omega.v2197logplain
-rw-r--r--Omega0.v2427logplain
-rw-r--r--Omega2.v763logplain
-rw-r--r--OmegaPre.v2195logplain
-rw-r--r--PCase.v1515logplain
-rw-r--r--PPFix.v207logplain
-rw-r--r--Print.v282logplain
-rw-r--r--PrintSortedUniverses.v39logplain
-rw-r--r--ProgramWf.v2278logplain
-rw-r--r--Projection.v1151logplain
-rw-r--r--ROmega.v2242logplain
-rw-r--r--ROmega0.v2542logplain
-rw-r--r--ROmega2.v982logplain
-rw-r--r--ROmegaPre.v2216logplain
-rw-r--r--RecTutorial.v25145logplain
-rw-r--r--Record.v2399logplain
-rw-r--r--Reg.v3062logplain
-rw-r--r--Remark.v172logplain
-rw-r--r--Rename.v220logplain
-rw-r--r--Reordering.v378logplain
-rw-r--r--Require.v88logplain
-rw-r--r--Scheme.v82logplain
-rw-r--r--Scopes.v454logplain
-rw-r--r--Section.v136logplain
-rw-r--r--Simplify_eq.v252logplain
-rw-r--r--Tauto.v5145logplain
-rw-r--r--TestRefine.v4317logplain
-rw-r--r--Try.v174logplain
-rw-r--r--Typeclasses.v1458logplain
-rw-r--r--apply.v11002logplain
-rw-r--r--auto.v548logplain
-rw-r--r--autointros.v462logplain
-rw-r--r--autorewrite.v763logplain
-rw-r--r--bullet.v53logplain
-rw-r--r--cc.v2331logplain
-rw-r--r--change.v1081logplain
-rw-r--r--clear.v290logplain
-rw-r--r--coercions.v3769logplain
-rw-r--r--conv_pbs.v7579logplain
-rw-r--r--coqbugs0181.v211logplain
-rw-r--r--decl_mode.v5537logplain
-rw-r--r--dependentind.v3932logplain
-rw-r--r--destruct.v1910logplain
-rw-r--r--eauto.v1867logplain
-rw-r--r--eqdecide.v819logplain
-rw-r--r--eta.v595logplain
-rw-r--r--evars.v12865logplain
-rw-r--r--extraction.v14186logplain
-rw-r--r--fix.v2168logplain
-rw-r--r--guard.v322logplain
-rw-r--r--hyps_inclusion.v1160logplain
-rw-r--r--if.v366logplain
-rw-r--r--implicit.v2763logplain
-rw-r--r--import_lib.v3415logplain
-rw-r--r--import_mod.v993logplain
-rw-r--r--inds_type_sec.v594logplain
-rw-r--r--induct.v1780logplain
-rw-r--r--instantiate.v293logplain
-rw-r--r--intros.v625logplain
-rw-r--r--ltac.v6110logplain
-rw-r--r--mutual_ind.v1601logplain
-rw-r--r--options.v690logplain
-rw-r--r--parsing.v218logplain
-rw-r--r--pattern.v1400logplain
-rw-r--r--polymorphism.v219logplain
-rw-r--r--proof_using.v708logplain
-rw-r--r--refine.v2672logplain
-rw-r--r--remember.v409logplain
-rw-r--r--replace.v635logplain
-rw-r--r--rewrite.v3306logplain
-rw-r--r--rewrite_in.v148logplain
-rw-r--r--rewrite_iterated.v545logplain
-rw-r--r--searchabout.v1690logplain
-rw-r--r--set.v408logplain
-rw-r--r--setoid_ring_module.v922logplain
-rw-r--r--setoid_test.v3916logplain
-rw-r--r--setoid_test2.v8251logplain
-rw-r--r--setoid_test_function_space.v1117logplain
-rw-r--r--simpl.v1232logplain
-rw-r--r--simpl_tuning.v3895logplain
-rw-r--r--specialize.v1416logplain
-rw-r--r--telescope_canonical.v2393logplain
-rw-r--r--unfold.v812logplain
-rw-r--r--unicode_utf8.v2215logplain
-rw-r--r--unification.v5958logplain
-rw-r--r--univers.v1575logplain
-rw-r--r--universes-coercion.v917logplain