aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2021-04-12[zify] More aggressive application of saturation rulesBESSON Frederic
2021-04-12Merge PR #14061: [zify] better error reportingVincent Laporte
2021-04-12[zify] better error reportingBESSON Frederic
2021-04-07Merge PR #14056: Miscellaneous mini-"typos" fixescoqbot-app[bot]
2021-04-07Merge PR #14008: [stdlib] [Arith] Cantor pairingcoqbot-app[bot]
2021-04-06Merge PR #14077: Add odoc warnings for empty packages.coqbot-app[bot]
2021-04-06Typo in ChoiceFacts.Hugo Herbelin
2021-04-06Standardizing spacing for {| ... |} in two files.Hugo Herbelin
2021-04-06Typo in a micromega comment.Hugo Herbelin
2021-04-06Add odoc warnings for empty packages.Théo Zimmermann
2021-04-02Remove the omega tactic and related optionsJim Fehrle
2021-04-02add Cantor pairing to_nat and its inverse of_natAndrej Dudenhefner
2021-03-31Merge PR #14022: Replace mentions of Num by Zarith.coqbot-app[bot]
2021-03-28Replace mentions of Num by Zarith.Guillaume Melquiond
2021-03-26remove in List.v deprecated/unnecessary dependencies: Le, Gt, Minus, Lt, SetoidAndrej Dudenhefner
2021-03-23add lemmas to List.v: Exists_map, Exists_concat, Exists_flat_map, Forall_map,...Andrej Dudenhefner
2021-03-23Merge PR #13671: [stdlib] [Vectors] add results on to_listcoqbot-app[bot]
2021-03-23Merge PR #13804: [stdlib] [List] Add results about count_occcoqbot-app[bot]
2021-03-19Merge PR #13730: Lint stdlib with -mangle-names #6coqbot-app[bot]
2021-03-16add results on to_listOlivier Laurent
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
2021-02-26Signed primitive integersAna
2021-02-25Merge PR #13080: Ascii: add leb and ltbcoqbot-app[bot]
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
2021-02-19Terminate some lemmas with Qed.Guillaume Melquiond
2021-01-29add results on count_occOlivier Laurent
2021-01-26Merge PR #13758: Remove the Hide Obligations flag (deprecated in 8.12)coqbot-app[bot]
2021-01-25Remove the Hide Obligations flagJim Fehrle
2021-01-20Use cbn instead of simpl in a proof of HexadecimalNat.Pierre-Marie Pédrot
2021-01-19Merge PR #13699: Fix #13579 (hnf on primitives raises an anomaly)Pierre-Marie Pédrot
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
2021-01-18Fix #13579 (hnf on primitives raises an anomaly)Pierre Roux
2021-01-08Modify Structures/OrderedType.v to compile with -mangle-namesJasper Hugunin
2021-01-08Modify Structures/DecidableType.v to compile with -mangle-namesJasper Hugunin
2021-01-08Modify Classes/SetoidDec.v to compile with -mangle-namesJasper Hugunin
2021-01-08Modify Classes/SetoidClass.v to compile with -mangle-namesJasper Hugunin
2021-01-08Modify Lists/SetoidList.v to compile with -mangle-namesJasper Hugunin
2021-01-08Modify Sorting/Sorted.v to compile with -mangle-namesJasper Hugunin
2021-01-08Modify Classes/EquivDec.v to compile with -mangle-namesJasper Hugunin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:59:08 +0000