aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2021-01-08Modify Program/Subset.v to compile with -mangle-namesJasper Hugunin
2021-01-08Modify Logic/ProofIrrelevanceFacts.v to compile with -mangle-namesJasper Hugunin
2021-01-02Deprecate "at ... with ..." in change tacticJim Fehrle
2020-12-24Merge PR #13649: Lint stdlib with -mangle-names #5coqbot-app[bot]
2020-12-15Modify Logic/JMeq.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify Program/Wf.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify Logic/FunctionalExtensionality.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify Classes/DecidableClass.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify Classes/CEquivalence.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify Bool/Zerob.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify Bool/IfProp.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify Bool/DecBool.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify Bool/BoolEq.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify Numbers/Cyclic/Int63/Int63.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify ZArith/Zgcd_alt.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify ZArith/Zpow_facts.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify ZArith/Zpower.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify micromega/ZMicromega.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify QArith/Qreduction.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify setoid_ring/Field_theory.v to compile with -mangle-namesJasper Hugunin
2020-12-15Modify QArith/QArith_base.v to compile with -mangle-namesJasper Hugunin
2020-12-15Catch up to where I was last time.Jasper Hugunin
2020-12-09Redefines exp_ineq1 to hold for all non-zero numbers.Avi Shinnar
2020-12-03Ascii: add leb and ltbYishuai Li
2020-12-02Merge PR #13275: Put all Int63 primitives in a separate fileVincent Laporte
2020-12-02Put all Int63 primitives in a separate filePierre Roux
2020-12-01Merge PR #13490: [ssr] Backport ssrbool from MathComp 1.12.0coqbot-app[bot]
2020-11-29Backport ssrbool lemmas from MathComp 1.12.0Kazuhiko Sakaguchi
2020-11-27Merge PR #13457: [RM] Update magicno & compatcoqbot-app[bot]
2020-11-25Merge PR #13228: [micromega] Performance of liaPierre-Marie Pédrot
2020-11-25Merge PR #13459: [ssr] Fixing [dup] and [swap] working around a bugcoqbot-app[bot]
2020-11-24Convert auto chapter to prodnJim Fehrle
2020-11-24Fixing [dup] and [swap]Cyril Cohen
2020-11-23Update compat infrastructure for 8.14Enrico Tassi
2020-11-22Adapting standard library, doc and test suite to ident->name renaming.Hugo Herbelin
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-18[micromega] Simplex uses alternatively Gomory cuts and case splitsBESSON Frederic
2020-11-18[micromega] Optimised cnf in case an hypothesis is trivially False.BESSON Frederic
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]
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 03:54:53 +0000