/test-suite/success/

• ../
• Abstract.v
• AdvancedCanonicalStructure.v
• AdvancedTypeClasses.v
• CanonicalStructure.v
• Case1.v
• Case10.v
• Case11.v
• Case12.v
• Case13.v
• Case14.v
• Case15.v
• Case16.v
• Case17.v
• Case18.v
• Case19.v
• Case2.v
• Case20.v
• Case21.v
• Case22.v
• Case3.v
• Case5.v
• Case6.v
• Case7.v
• Case8.v
• Case9.v
• CaseAlias.v
• CaseInClause.v
• Cases-bug1834.v
• Cases-bug3758.v
• Cases.v
• CasesDep.v
• Check.v
• Conjecture.v
• DHyp.v
• Decompose.v
• DiscrR.v
• Discriminate.v
• Field.v
• Fixpoint.v
• Fourier.v
• Funind.v
• FunindExtraction_compat86.v
• Generalization.v
• Generalize.v
• Hints.v
• ImplicitArguments.v
• ImplicitTactic.v
• Import.v
• Inductive.v
• Injection.v
• Inversion.v
• InversionSigma.v
• LetIn.v
• LetPat.v
• MatchFail.v
• Mod_ltac.v
• Mod_params.v
• Mod_strengthen.v
• Mod_type.v
• NatRing.v
• Notations.v
• Notations2.v
• Nsatz.v
• NumberScopes.v
• Omega.v
• Omega0.v
• Omega2.v
• OmegaPre.v
• PCase.v
• PPFix.v
• PatternsInBinders.v
• Print.v
• PrintSortedUniverses.v
• ProgramWf.v
• Projection.v
• ROmega.v
• ROmega0.v
• ROmega2.v
• ROmega3.v
• ROmega4.v
• ROmegaPre.v
• RecTutorial.v
• Record.v
• Reg.v
• Remark.v
• Rename.v
• Reordering.v
• Require.v
• Scheme.v
• Scopes.v
• Section.v
• Simplify_eq.v
• TacticNotation1.v
• TacticNotation2.v
• Tauto.v
• TestRefine.v
• Try.v
• Typeclasses.v
• abstract_chain.v
• abstract_poly.v
• all-check.v
• apply.v
• applyTC.v
• auto.v
• autointros.v
• autorewrite.v
• boundvars.v
• bteauto.v
• bullet.v
• cbn.v
• cc.v
• change.v
• change_pattern.v
• clear.v
• coercions.v
• coindprim.v
• contradiction.v
• conv_pbs.v
• coqbugs0181.v
• cumulativity.v
• dependentind.v
• destruct.v
• eauto.v
• eqdecide.v
• eta.v
• evars.v
• extraction.v
• extraction_dep.v
• extraction_impl.v
• extraction_polyprop.v
• fix.v
• forward.v
• goal_selector.v
• guard.v
• hintdb_in_ltac.v
• hintdb_in_ltac_bis.v
• hyps_inclusion.v
• if.v
• implicit.v
• import_lib.v
• import_mod.v
• indelim.v
• inds_type_sec.v
• induct.v
• intros.v
• keyedrewrite.v
• letproj.v
• ltac.v
• ltac_match_pattern_names.v
• ltac_plus.v
• ltacprof.v
• mutual_ind.v
• namedunivs.v
• old_typeclass.v
• onlyprinting.v
• options.v
• par_abstract.v
• paralleltac.v
• parsing.v
• pattern.v
• polymorphism.v
• primitiveproj.v
• programequality.v
• proof_using.v
• record_syntax.v
• refine.v
• remember.v
• replace.v
• rewrite.v
• rewrite_dep.v
• rewrite_evar.v
• rewrite_in.v
• rewrite_iterated.v
• rewrite_strat.v
• searchabout.v
• set.v
• setoid_ring_module.v
• setoid_test.v
• setoid_test2.v
• setoid_test_function_space.v
• setoid_unif.v
• shrink_abstract.v
• shrink_obligations.v
• sideff.v
• simpl.v
• simpl_tuning.v
• somatching.v
• specialize.v
• ssrpattern.v
• subst.v
• telescope_canonical.v
• transparent_abstract.v
• tryif.v
• unfold.v
• unicode_utf8.v
• unidecls.v
• unification.v
• univers.v
• universes-coercion.v
• univnames.v
• univscompute.v
• unshelve.v
• vm_univ_poly.v
• vm_univ_poly_match.v