aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
2021-02-25Merge PR #13080: Ascii: add leb and ltbcoqbot-app[bot]
Reviewed-by: anton-trunov
2021-02-20Inline proofs of exist_exp0 and exist_cos0.Guillaume Melquiond
2021-02-19Remove some trivial definition.Guillaume Melquiond
2021-02-19Abstract the non-computational part away.Guillaume Melquiond
2021-02-19Terminate intermediate lemmas with Qed.Guillaume Melquiond
2021-02-19Make intermediate lemmas more explicit, so that they can be terminated by Qed.Guillaume Melquiond
2021-02-19Make most of DRealAbstr opaque.Guillaume Melquiond
The function returned by DRealAbstr starts by a call to the axiom sig_forall_dec, so it is not computable anyway.
2021-02-19Terminate some lemmas with Qed.Guillaume Melquiond
Since the proofs start by applying or destructuring Qed-ed lemmas, they cannot be used in a computational setting, so no need for them to be Defined.
2021-01-26Merge PR #13758: Remove the Hide Obligations flag (deprecated in 8.12)coqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2021-01-25Remove the Hide Obligations flagJim Fehrle
2021-01-20Use cbn instead of simpl in a proof of HexadecimalNat.Pierre-Marie Pédrot
This reduces the tactic invocation time from 10s to 0.25s on my machine. I was growing tired of having to wait for that file while compiling the stdlib.
2021-01-19Merge PR #13699: Fix #13579 (hnf on primitives raises an anomaly)Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
We deprecate unspecified locality as was done for Hint. Close #13724
2021-01-18Fix #13579 (hnf on primitives raises an anomaly)Pierre Roux
Also works for simpl.
2021-01-02Deprecate "at ... with ..." in change tacticJim Fehrle
(use "with ... at ..." instead)
2020-12-24Merge PR #13649: Lint stdlib with -mangle-names #5coqbot-app[bot]
Reviewed-by: anton-trunov
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
Many of the changes are a consequence of coq/coq#13132.
2020-12-09Redefines exp_ineq1 to hold for all non-zero numbers.Avi Shinnar
The original (which holds only for positive numbers) is now called exp_ineq1_pos. A version that holds only for negative numbers is added as exp_ineq1_neg. Adds exp_ineq1_le, which holds for all reals (but is a <= instead of a <). Co-authored-by: Barry M. Trager <bmt@us.ibm.com>
2020-12-03Ascii: add leb and ltbYishuai Li
2020-12-02Merge PR #13275: Put all Int63 primitives in a separate fileVincent Laporte
Ack-by: SkySkimmer Ack-by: ppedrot Reviewed-by: vbgl
2020-12-02Put all Int63 primitives in a separate filePierre Roux
Following a request from Pierre-Marie Pédrot in #13258
2020-12-01Merge PR #13490: [ssr] Backport ssrbool from MathComp 1.12.0coqbot-app[bot]
Reviewed-by: gares
2020-11-29Backport ssrbool lemmas from MathComp 1.12.0Kazuhiko Sakaguchi
2020-11-27Merge PR #13457: [RM] Update magicno & compatcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-25Merge PR #13228: [micromega] Performance of liaPierre-Marie Pédrot
Reviewed-by: ppedrot Ack-by: vbgl
2020-11-25Merge PR #13459: [ssr] Fixing [dup] and [swap] working around a bugcoqbot-app[bot]
Reviewed-by: gares
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]
Reviewed-by: CohenCyril
2020-11-20[doc] [ssr] fix documentation of reflectEnrico Tassi
2020-11-18[micromega] Simplex uses alternatively Gomory cuts and case splitsBESSON Frederic
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-12 04:47:00 +0000