Tree @71cfeb92-b044-4a1f-8a28-dbfac04aa818/main (Download .tar.gz)

• ..
• Abstract.v
• abstract_chain.v
• abstract_poly.v
• AdvancedCanonicalStructure.v
• AdvancedTypeClasses.v
• all_check.v
• apply.v
• applyTC.v
• attribute_syntax.v
• auto.v
• autointros.v
• autorewrite.v
• BidirectionalityHints.v
• boundvars.v
• BracketsWithGoalSelector.v
• btauto.v
• bteauto.v
• bug_10890.v
• bug_14174.v
• bullet.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
• Case4.v
• Case5.v
• Case6.v
• Case7.v
• Case8.v
• Case9.v
• case_let_conversion.v
• case_let_param.v
• CaseAlias.v
• CaseInClause.v
• Cases.v
• Cases_bug1834.v
• Cases_bug3758.v
• CasesDep.v
• cbn.v
• cbv_let.v
• cc.v
• change.v
• change_case.v
• change_pattern.v
• Check.v
• clear.v
• coercions.v
• cofixtac.v
• coindprim.v
• CombinedScheme.v
• CompatCurrentFlag.v
• CompatOldFlag.v
• CompatPreviousFlag.v
• Conjecture.v
• contradiction.v
• conv_pbs.v
• ConversionOrder.v
• coqbugs0181.v
• cumulativity.v
• CumulInd.v
• custom_entry.v
• Decompose.v
• definition_using.v
• dependentind.v
• destruct.v
• DHyp.v
• Discriminate.v
• Discriminate_HoTT.v
• DiscrR.v
• dtauto_let_deps.v
• eapply_evar.v
• eauto.v
• eqdecide.v
• eqtacticsnois.v
• eta.v
• evars.v
• export_hint.v
• export_inst.v
• extraction.v
• extraction_dep.v
• extraction_impl.v
• extraction_polyprop.v
• Field.v
• fix.v
• Fixpoint.v
• forward.v
• Funind.v
• Generalization.v
• Generalize.v
• goal_selector.v
• guard.v
• hint_discr_unfold.v
• hintdb_in_ltac.v
• hintdb_in_ltac_bis.v
• HintMode.v
• Hints.v
• hyps_inclusion.v
• if.v
• implicit.v
• ImplicitArguments.v
• Import.v
• import_lib.v
• import_mod.v
• ImportCat.v
• indelim.v
• inds_type_sec.v
• induct.v
• Inductive.v
• InductiveVsImplicitsVsTC.v
• Injection.v
• intros.v
• Inversion.v
• InversionSigma.v
• keyedrewrite.v
• let_pattern_mismatch.v
• let_universes.v
• LetIn.v
• LetPat.v
• letproj.v
• LocalDefinition.v
• LraTest.v
• ltac.v
• ltac_match_pattern_names.v
• ltac_plus.v
• LtacDeprecation.v
• ltacprof.v
• MangleNamesLight.v
• match_case_pattern_variables.v
• MatchFail.v
• Mod_ltac.v
• Mod_params.v
• Mod_strengthen.v
• Mod_type.v
• module_with_def_univ_poly.v
• mutual_ind.v
• mutual_record.v
• name_mangling.v
• namedunivs.v
• NatRing.v
• Nia.v
• NotationDeprecation.v
• Notations.v
• Notations2.v
• NotationsAndLtac.v
• Nsatz.v
• NumberNotationsNoLocal.v
• NumberScopes.v
• Omega.v
• Omega0.v
• Omega2.v
• OmegaPre.v
• onlyprinting.v
• options.v
• par_abstract.v
• paralleltac.v
• parsing.v
• PartialImport.v
• pattern.v
• PatternsInBinders.v
• PCase.v
• polymorphism.v
• pose.v
• PPFix.v
• primitive.v
• primitiveproj.v
• Print.v
• PrintSortedUniverses.v
• private_univs.v
• programequality.v
• ProgramWf.v
• Projection.v
• proof_using.v
• proof_using_noinit.v
• rapply.v
• Record.v
• record_syntax.v
• RecTutorial.v
• refine.v
• RefineInstance.v
• Reg.v
• Remark.v
• remember.v
• RemoteUnivs.v
• Rename.v
• Reordering.v
• replace.v
• Require.v
• rewrite.v
• rewrite_closed.v
• rewrite_dep.v
• rewrite_evar.v
• rewrite_in.v
• rewrite_iterated.v
• rewrite_strat.v
• RewriteRegisteredElim.v
• ROmega.v
• ROmega0.v
• ROmega2.v
• ROmega4.v
• ROmegaPre.v
• Scheme.v
• SchemeEquality.v
• Scopes.v
• search.v
• Section.v
• section_poly.v
• set.v
• setoid_ring_module.v
• setoid_test.v
• setoid_test2.v
• setoid_test_function_space.v
• setoid_unif.v
• ShowExtraction.v
• shrink_abstract.v
• shrink_obligations.v
• sideff.v
• simpl.v
• simpl_tuning.v
• simple_congruence.v
• Simplify_eq.v
• somatching.v
• specialize.v
• sprop.v
• sprop_hcons.v
• sprop_uip.v
• ssrpattern.v
• strategy.v
• StuckHintMode.v
• subst.v
• tac_wit_ref.v
• TacticNotation1.v
• TacticNotation2.v
• Tauto.v
• TCbacktrack.v
• telescope_canonical.v
• Template.v
• TestRefine.v
• transparent_abstract.v
• Try.v
• tryif.v
• Typeclasses.v
• Typeclasses_eauto_dfs_bfs.v
• TypeclassesOpaque.v
• typing_flags.v
• unfold.v
• unicode_utf8.v
• unidecls.v
• unification.v
• unification_delta.v
• uniform_inductive_parameters.v
• univers.v
• universes_coercion.v
• univnames.v
• univscompute.v
• unshelve.v
• vm_evars.v
• vm_records.v
• vm_univ_poly.v
• vm_univ_poly_match.v
• with_strategy.v