aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
ModeNameSize
-rw-r--r--Abstract.v438logplain
-rw-r--r--AdvancedCanonicalStructure.v3365logplain
-rw-r--r--AdvancedTypeClasses.v2235logplain
-rw-r--r--BracketsWithGoalSelector.v371logplain
-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.v2476logplain
-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.v970logplain
-rw-r--r--Case2.v306logplain
-rw-r--r--Case20.v1106logplain
-rw-r--r--Case21.v476logplain
-rw-r--r--Case22.v2646logplain
-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.v984logplain
-rw-r--r--Cases-bug1834.v383logplain
-rw-r--r--Cases-bug3758.v386logplain
-rw-r--r--Cases.v39497logplain
-rw-r--r--CasesDep.v14537logplain
-rw-r--r--Check.v964logplain
-rw-r--r--Conjecture.v231logplain
-rw-r--r--DHyp.v1logplain
-rw-r--r--Decompose.v218logplain
-rw-r--r--DiscrR.v435logplain
-rw-r--r--Discriminate.v822logplain
-rw-r--r--Field.v2128logplain
-rw-r--r--Fixpoint.v2977logplain
-rw-r--r--Funind.v10180logplain
-rw-r--r--FunindExtraction_compat86.v10204logplain
-rw-r--r--Generalization.v282logplain
-rw-r--r--Generalize.v176logplain
-rw-r--r--Hints.v5999logplain
-rw-r--r--ImplicitArguments.v1053logplain
-rw-r--r--Import.v218logplain
-rw-r--r--Inductive.v6083logplain
-rw-r--r--Injection.v4023logplain
-rw-r--r--Inversion.v5366logplain
-rw-r--r--InversionSigma.v1574logplain
-rw-r--r--LetIn.v356logplain
-rw-r--r--LetPat.v1760logplain
-rw-r--r--LraTest.v285logplain
-rw-r--r--LtacDeprecation.v473logplain
-rw-r--r--MatchFail.v844logplain
-rw-r--r--Mod_ltac.v302logplain
-rw-r--r--Mod_params.v1375logplain
-rw-r--r--Mod_strengthen.v963logplain
-rw-r--r--Mod_type.v515logplain
-rw-r--r--NatRing.v125logplain
-rw-r--r--Notations.v4808logplain
-rw-r--r--Notations2.v6138logplain
-rw-r--r--Nsatz.v14291logplain
-rw-r--r--NumberScopes.v921logplain
-rw-r--r--Omega.v2193logplain
-rw-r--r--Omega0.v2429logplain
-rw-r--r--Omega2.v765logplain
-rw-r--r--OmegaPre.v2195logplain
-rw-r--r--PCase.v1515logplain
-rw-r--r--PPFix.v207logplain
-rw-r--r--PatternsInBinders.v1426logplain
-rw-r--r--Print.v282logplain
-rw-r--r--PrintSortedUniverses.v39logplain
-rw-r--r--ProgramWf.v2279logplain
-rw-r--r--Projection.v1278logplain
-rw-r--r--ROmega.v2238logplain
-rw-r--r--ROmega0.v2757logplain
-rw-r--r--ROmega2.v984logplain
-rw-r--r--ROmega3.v872logplain
-rw-r--r--ROmega4.v488logplain
-rw-r--r--ROmegaPre.v2216logplain
-rw-r--r--RecTutorial.v25138logplain
-rw-r--r--Record.v2598logplain
-rw-r--r--Reg.v3062logplain
-rw-r--r--Remark.v172logplain
-rw-r--r--Rename.v222logplain
-rw-r--r--Reordering.v378logplain
-rw-r--r--Require.v88logplain
-rw-r--r--Scheme.v593logplain
-rw-r--r--Scopes.v561logplain
-rw-r--r--Section.v136logplain
-rw-r--r--ShowExtraction.v592logplain
-rw-r--r--Simplify_eq.v252logplain
-rw-r--r--TacticNotation1.v198logplain
-rw-r--r--TacticNotation2.v310logplain
-rw-r--r--Tauto.v5295logplain
-rw-r--r--TestRefine.v4465logplain
-rw-r--r--Try.v172logplain
-rw-r--r--Typeclasses.v6713logplain
-rw-r--r--abstract_chain.v885logplain
-rw-r--r--abstract_poly.v513logplain
-rw-r--r--all-check.v36logplain
-rw-r--r--apply.v14140logplain
-rw-r--r--applyTC.v289logplain
-rw-r--r--attribute-syntax.v356logplain
-rw-r--r--auto.v3284logplain
-rw-r--r--autointros.v462logplain
-rw-r--r--autorewrite.v763logplain
-rw-r--r--boundvars.v621logplain
-rw-r--r--bteauto.v4062logplain
-rw-r--r--bullet.v53logplain
-rw-r--r--cbn.v317logplain
-rw-r--r--cc.v3472logplain
-rw-r--r--change.v1853logplain
-rw-r--r--change_pattern.v1244logplain
-rw-r--r--clear.v568logplain
-rw-r--r--coercions.v5022logplain
-rw-r--r--coindprim.v2826logplain
-rw-r--r--contradiction.v563logplain
-rw-r--r--conv_pbs.v7579logplain
-rw-r--r--coqbugs0181.v211logplain
-rw-r--r--cumulativity.v4162logplain
-rw-r--r--dependentind.v3924logplain
-rw-r--r--destruct.v9888logplain
-rw-r--r--dtauto-let-deps.v792logplain
-rw-r--r--eauto.v5790logplain
-rw-r--r--eqdecide.v1188logplain
-rw-r--r--eta.v595logplain
-rw-r--r--evars.v13575logplain
-rw-r--r--extraction.v15165logplain
-rw-r--r--extraction_dep.v991logplain
-rw-r--r--extraction_impl.v1922logplain
-rw-r--r--extraction_polyprop.v398logplain
-rw-r--r--fix.v2182logplain
-rw-r--r--forward.v664logplain
-rw-r--r--goal_selector.v1416logplain
-rw-r--r--guard.v828logplain
-rw-r--r--hintdb_in_ltac.v275logplain
-rw-r--r--hintdb_in_ltac_bis.v237logplain
-rw-r--r--hyps_inclusion.v1160logplain
-rw-r--r--if.v365logplain
-rw-r--r--implicit.v2768logplain
-rw-r--r--import_lib.v3415logplain
-rw-r--r--import_mod.v993logplain
-rw-r--r--indelim.v1360logplain
-rw-r--r--inds_type_sec.v744logplain
-rw-r--r--induct.v5043logplain
-rw-r--r--intros.v3285logplain
-rw-r--r--keyedrewrite.v1384logplain
-rw-r--r--letproj.v307logplain
-rw-r--r--ltac.v7320logplain
-rw-r--r--ltac_match_pattern_names.v604logplain
-rw-r--r--ltac_plus.v357logplain
-rw-r--r--ltacprof.v223logplain
-rw-r--r--mutual_ind.v1751logplain
-rw-r--r--mutual_record.v753logplain
-rw-r--r--name_mangling.v3289logplain
-rw-r--r--namedunivs.v2799logplain
-rw-r--r--onlyprinting.v150logplain
-rw-r--r--options.v690logplain
-rw-r--r--par_abstract.v469logplain
-rw-r--r--paralleltac.v1193logplain
-rw-r--r--parsing.v218logplain
-rw-r--r--pattern.v1400logplain
-rw-r--r--polymorphism.v11008logplain
-rw-r--r--primitiveproj.v5329logplain
-rw-r--r--programequality.v267logplain
-rw-r--r--proof_using.v2575logplain
-rw-r--r--record_syntax.v920logplain
-rw-r--r--refine.v2992logplain
-rw-r--r--remember.v626logplain
-rw-r--r--replace.v635logplain
-rw-r--r--rewrite.v4318logplain
-rw-r--r--rewrite_dep.v930logplain
-rw-r--r--rewrite_evar.v376logplain
-rw-r--r--rewrite_in.v148logplain
-rw-r--r--rewrite_iterated.v545logplain
-rw-r--r--rewrite_strat.v1275logplain
-rw-r--r--searchabout.v1690logplain
-rw-r--r--set.v408logplain
-rw-r--r--setoid_ring_module.v922logplain
-rw-r--r--setoid_test.v4488logplain
-rw-r--r--setoid_test2.v8535logplain
-rw-r--r--setoid_test_function_space.v1117logplain
-rw-r--r--setoid_unif.v911logplain
-rw-r--r--shrink_abstract.v198logplain
-rw-r--r--shrink_obligations.v605logplain
-rw-r--r--sideff.v305logplain
-rw-r--r--simpl.v2693logplain
-rw-r--r--simpl_tuning.v3897logplain
-rw-r--r--somatching.v1534logplain
-rw-r--r--specialize.v3465logplain
-rw-r--r--ssr_delayed_clear_rename.v128logplain
-rw-r--r--ssrpattern.v514logplain
-rw-r--r--subst.v984logplain
-rw-r--r--telescope_canonical.v2393logplain
-rw-r--r--transparent_abstract.v800logplain
-rw-r--r--tryif.v1331logplain
-rw-r--r--unfold.v962logplain
-rw-r--r--unicode_utf8.v2216logplain
-rw-r--r--unidecls.v2228logplain
-rw-r--r--unification.v6301logplain
-rw-r--r--uniform_inductive_parameters.v384logplain
-rw-r--r--univers.v1942logplain
-rw-r--r--universes-coercion.v917logplain
-rw-r--r--univnames.v904logplain
-rw-r--r--univscompute.v721logplain
-rw-r--r--unshelve.v401logplain
-rw-r--r--vm_evars.v348logplain
-rw-r--r--vm_records.v635logplain
-rw-r--r--vm_univ_poly.v4178logplain
-rw-r--r--vm_univ_poly_match.v606logplain