aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2020-11-20Merge PR #13426: [doc] [ssr] fix documentation of reflectcoqbot-app[bot]
2020-11-20[doc] [ssr] fix documentation of reflectEnrico Tassi
2020-11-16Improve some error messages.Vincent Semeria
2020-11-16Merge PR #13384: Warn on hints without an explicit localitycoqbot-app[bot]
2020-11-16Merge PR #13188: Default disable automatic generalization of Instance typePierre-Marie Pédrot
2020-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
2020-11-16Merge PR #13365: Fix proof of Coq.Program.Wf.Fix_F_inv to be axiom-freecoqbot-app[bot]
2020-11-15Update compate Coq812.vGaëtan Gilbert
2020-11-15Default disable automatic generalization of Instance typeGaëtan Gilbert
2020-11-13Merge PR #12420: [stdlib] Decidable instance for negationcoqbot-app[bot]
2020-11-13Fix proof of Coq.Program.Wf.Fix_F_inv to be axiom-freeLi-yao Xia
2020-11-12Merge PR #13318: Turn ssr proxy notation for supporting second-order/contextu...coqbot-app[bot]
2020-11-12Merge PR #13317: [ssr] intro pattern extensions for dup, swap and applycoqbot-app[bot]
2020-11-09[compat] remove 8.10Enrico Tassi
2020-11-09Merge PR #13173: Lint stdlib with -mangle-names #4coqbot-app[bot]
2020-11-06Intro pattern extensions for dup, swap and applyCyril Cohen
2020-11-06The "( X in t )" hack used in the syntax of ssr rewrite may be only parsing.Hugo Herbelin
2020-11-04[stdlib] Decidable instance for negationYishuai Li
2020-11-05Rename Dec and HexDec to Decimal and HexadecimalPierre Roux
2020-11-05Merge numeral and string notation pluginsPierre Roux
2020-11-05[numeral notation] Prove RPierre Roux
2020-11-05[numeral notation] Specify RPierre Roux
2020-11-05[numeral notation] RPierre Roux
2020-11-05[numeral notation] Prove QPierre Roux
2020-11-05[numeral notation] Specify QPierre Roux
2020-11-05[numeral notation] QPierre Roux
2020-11-05[numeral notation] Remove proofs for QPierre Roux
2020-11-04[numeral notation] Adding the via ... using ... optionPierre Roux
2020-10-30Renaming Numeral.v into Number.vPierre Roux
2020-10-26Merge PR #12768: Granting wish #12762: warning on duplicated catch-all patter...coqbot-app[bot]
2020-10-21Merge PR #13201: Report a useful error for dependent destructionPierre-Marie Pédrot
2020-10-21Merge PR #12955: Reroot primitive arrays on accesscoqbot-app[bot]
2020-10-20[zify] Use flag for Z.to_euclidean_division_equations.Frédéric Besson
2020-10-20[zify] Add support for Int63.intFrédéric Besson
2020-10-15Consistent indentation + a few bullets in RIneq.v.Hugo Herbelin
2020-10-15Report a useful error for dependent destructionTej Chajed
2020-10-11Modify ZArith/Znumtheory.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Zdiv.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Zcomplements.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/ZifyInst.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/ZifyClasses.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/Ztac.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/ZCoeff.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Zpow_def.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Wf_Z.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Zabs.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Znat.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/RingMicromega.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/Tauto.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/Refl.v to compile with -mangle-namesJasper Hugunin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:45:01 +0000