aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-09-17[ci/gitlab/cachix] Avoid running in trouble when calling git fetch --unshallow.Théo Zimmermann
2020-09-17Merge PR #13007: [build] Don't link `num` anymore in Coqcoqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: vbgl Ack-by: Zimmi48 Ack-by: vbgl
2020-09-17[configure] Fix version checks for lablgtk and zarithEmilio Jesus Gallego Arias
Fixes #13041 #13047 Configure is quite messy, but we will improve it once we can link it with findlib and move to dune [that will actually allow to remove all ad-hoc calls to `ocamlfind` in favor of `findlib` code.
2020-09-17Be more efficient when generating the merge of ltle maps in AcyclicGraph.Pierre-Marie Pédrot
We try to avoid reallocating the map in two different ways. - We only add a value when actually needed. - We compute the union of maps with the first element as a starting point.
2020-09-17Do not allocate intermediate sets in universe refreshing.Pierre-Marie Pédrot
A set was created only to be folded over. Since the list is ensured to be duplicate-free, there is no point in creating the former, we just fold over the list directly.
2020-09-17[leminv] Use higher-level Declare API.Emilio Jesus Gallego Arias
2020-09-17[leminv] Remove unused catch.Emilio Jesus Gallego Arias
2020-09-17[install] Rewording of primitive floats.Emilio Jesus Gallego Arias
As suggested in the PR review. Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-09-17[build] Don't link `num` anymore in CoqEmilio Jesus Gallego Arias
After #8743 we don't depend on `num` anymore in the codebase; thus we drop the dependency. This could create problems for plugins relying on this implicit linking.
2020-09-17Merge PR #13024: [CI] Always upload artifactscoqbot-app[bot]
Reviewed-by: Zimmi48
2020-09-17[ci] call dmesg after quick/async jobs to detect OOMEnrico Tassi
2020-09-17Formally deprecate the double induction tactic.Pierre-Marie Pédrot
The doc states it is deprecated since 1386cd9 but this was ages before the deprecation mechanism existed.
2020-09-16Modify setoid_ring/BinList.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Lists/List.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify setoid_ring/Ring_theory.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify NArith/Nnat.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify PArith/Pnat.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify NArith/BinNat.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify PArith/BinPos.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Arith/Wf_nat.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Arith/EqNat.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Arith/Factorial.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Arith/Compare_dec.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Arith/Peano_dec.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Logic/Eqdep_dec.v to compile with -vJasper Hugunin
2020-09-16Modify Logic/EqdepFacts.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Arith/Between.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Arith/Mult.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Arith/Plus.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Arith/Le.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Arith/PeanoNat.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NBits.v to compile with -mangle-namesJasper Hugunin
The bitwise tactic was performing `intros ?m`, and the name m got used later in many proofs. I defined a tactic notation `bitwise as m` to be able to provide the name for `m` explicitly. I did not make the notation local, because it seems like it would be useful for any clients using `bitwise` who want to avoid generated names. I have relatively little experience with writing Ltac and tactic notations, so if my solution can be improved, please show me how.
2020-09-16Modify Numbers/Natural/Abstract/NLcm.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NGcd.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NDiv.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NPow.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NParity.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NMaxMin.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NSub.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NAddOrder.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NOrder.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NAdd.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NBase.v to compile with -mangle-namesJasper Hugunin
2020-09-16Merge PR #13008: Use fresher names in eqschemesHugo Herbelin
Reviewed-by: herbelin Reviewed-by: ppedrot
2020-09-16Merge PR #13015: Propagate zarith dependency.Vincent Laporte
Reviewed-by: vbgl
2020-09-16Merge PR #8743: [micromega] Switch from `Big_int` to ZArith.BESSON Frederic
Ack-by: JasonGross Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: fajb Ack-by: liyishuai Ack-by: maximedenes Ack-by: ppedrot Ack-by: soraros Ack-by: thery Ack-by: vbgl
2020-09-16More improvements in locating tactic errors.Hugo Herbelin
We finally pass the location in the "ist", and keep it in the "VFun" which is associated to expanded Ltac constants.
2020-09-15[vernac] Don't allow attributes on print / checkEmilio Jesus Gallego Arias
Fixes #11661
2020-09-15Adding change log for #13026.Hugo Herbelin
2020-09-15A temporary fix of #13018 and #12775 for branch 8.2.Hugo Herbelin
We arbitrarily use max_int as higher level of custom entries in printing, which should be ok since only < and <= are used to decide when to use coercions.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 23:18:41 +0000