aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-15[micromega] Use `minus_one` built-in zarith constant.Emilio Jesus Gallego Arias
2020-09-15[zarith] [micromega] Bump to 1.10 and remove some hacksEmilio Jesus Gallego Arias
In particular, behavior of `Z.gcd` and `Z.lcm` has been fixed in 1.10, see https://github.com/ocaml/Zarith/issues/58
2020-09-15Updated .csdp.cache.test-suite and minor fixesBESSON Frederic
- merlin.in : added zarith - test-suite/Makefile remove .csdp.cache on make clean updated .csdp.cache.test-suite
2020-09-15[micromega] [test-suite] Update csdp cache for num -> zarith migrationEmilio Jesus Gallego Arias
2020-09-15[micromega] Migrate from num to zarithEmilio Jesus Gallego Arias
We still link num in `coqc` , that will be removed in a separate step. Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
2020-09-15[micromega] call csdpcert using path.Emilio Jesus Gallego Arias
2020-09-15Merge PR #13016: Remove deprecated Extraction Language command value "Ocaml"Pierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: pi8027 Reviewed-by: ppedrot
2020-09-15Merge PR #12972: [ci] [docker] Up testing to OCaml 4.11.1coqbot-app[bot]
Reviewed-by: Zimmi48
2020-09-14Remove deprecated Extraction Language command value "Ocaml"Jim Fehrle
2020-09-14[nix] Update ref for ocamlformat 0.15Emilio Jesus Gallego Arias
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-09-14[ocamlformat] Update to ocamlformat 0.15.0Emilio Jesus Gallego Arias
This is necessary to support OCaml 4.11 in development.
2020-09-14[ci] [docker] Up testing to OCaml 4.11.1Emilio Jesus Gallego Arias
- `odoc` must be bumped to support 4.11
2020-09-14Merge PR #13014: [ci] [mathcomp] run the test suitecoqbot-app[bot]
Reviewed-by: Zimmi48
2020-09-14Merge PR #13022: Fixing documentation relatively to example of use of extra ↵coqbot-app[bot]
spaces in notations Reviewed-by: jfehrle
2020-09-13Fixing documentation relatively to example of use of extra spaces in notations.Hugo Herbelin
2020-09-12Merge PR #12979: Uniformize names for number literals between parsing and refmancoqbot-app[bot]
Reviewed-by: herbelin Reviewed-by: jfehrle Ack-by: Zimmi48 Ack-by: proux01
2020-09-11[numeral notation] Improve documentationPierre Roux
Following reviews from Jim Fehrle on #12218 and #12979
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 15:33:46 +0000