aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
2020-11-09[compat] remove 8.10Enrico Tassi
2020-11-09Merge PR #13173: Lint stdlib with -mangle-names #4coqbot-app[bot]
Reviewed-by: anton-trunov
2020-11-06Intro pattern extensions for dup, swap and applyCyril Cohen
2020-11-06The "( X in t )" hack used in the syntax of ssr rewrite may be only parsing.Hugo Herbelin
This is the only notation to date which breaks the heuristics of prefering the more precise notations for printing (see #12986).
2020-11-04[stdlib] Decidable instance for negationYishuai Li
Added Changelog
2020-11-05Rename Dec and HexDec to Decimal and HexadecimalPierre Roux
As noted by Hugo Herbelin, Dec is rather used for "decidable".
2020-11-05Merge numeral and string notation pluginsPierre Roux
2020-11-05[numeral notation] Prove RPierre Roux
2020-11-05[numeral notation] Specify RPierre Roux
2020-11-05[numeral notation] RPierre Roux
Previously real constants were parsed by an unproved OCaml code. The parser and printer are now implemented in Coq, which will enable a proof and hopefully make it easier to maintain / make evolve. Previously reals were all parsed as an integer, an integer multiplied by a power of ten or an integer divided by a power of ten. This means 1.02 and 102e-2 were both parsed as 102 / 100 and could not be tell apart when printing. So the printer had to choose between two representations : without exponent or without decimal dot. The choice was made heuristically toward a most compact representation. Now, decimal dot is parsed as a rational and exponents are parsed as a product or division by a power of ten. For instance, 1.02 is parsed as Q2R (102 # 100) whereas 102e-2 is parsed as IZR 102 / IZR (Z.pow_pos 10 2). 1.02 and 102e-2 remain equal (proved by reflexivity) but 1.02e1 = Q2R (102 # 100) * 10 and 10.2 = Q2R (102 # 10) no longer are.
2020-11-05[numeral notation] Prove QPierre Roux
2020-11-05[numeral notation] Specify QPierre Roux
2020-11-05[numeral notation] QPierre Roux
Previously rationals were all parsed as a pair numerator, denominator. This means 1.02 and 102e-2 were both parsed as 102 # 100 and could not be tell apart when printing. So the printer had to choose between two representations : without exponent or without decimal dot. The choice was made heuristically toward a most compact representation. Now, decimal dot is still parsed as a power of ten denominator but exponents are parsed as a product or division by Z.pow_pos. For instance, 1.02 is parsed as 102 # 100 whereas 102e-2 is parsed as (102 # 1) / (Z.pow_pos 10 2 # 1). 1.02 and 102e-2 remain equal (proved by reflexivity) but 1.02e1 = (102 # 100) * (10 # 1) = 1020 # 100 and 10.2 = 102 # 10 no longer are. A nice side effect is that exponents can no longer blow up during parsing. Previously 1e1_000_000 literally produced a numerator with a million digits, now it just yields (1 # 1) * (Z.pow_pos 10 1_000_000 # 1).
2020-11-05[numeral notation] Remove proofs for QPierre Roux
Just to get a cleaner log, this will be proved again in a few commits.
2020-11-04[numeral notation] Adding the via ... using ... optionPierre Roux
This enables numeral notations for non inductive types by pre/postprocessing them to a given proxy inductive type. For instance, this should enable the use of numeral notations for R.
2020-10-30Renaming Numeral.v into Number.vPierre Roux
2020-10-26Merge PR #12768: Granting wish #12762: warning on duplicated catch-all ↵coqbot-app[bot]
pattern-matching clause with unused named variable Reviewed-by: jfehrle Reviewed-by: vbgl Ack-by: gares
2020-10-21Merge PR #13201: Report a useful error for dependent destructionPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-21Merge PR #12955: Reroot primitive arrays on accesscoqbot-app[bot]
Reviewed-by: maximedenes
2020-10-20[zify] Use flag for Z.to_euclidean_division_equations.Frédéric Besson
Update doc/sphinx/addendum/micromega.rst Co-authored-by: Jason Gross <jasongross9@gmail.com> Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-10-20[zify] Add support for Int63.intFrédéric Besson
Update doc/sphinx/addendum/micromega.rst Co-authored-by: Jason Gross <jasongross9@gmail.com> Update theories/micromega/ZifyInt63.v Co-authored-by: Jason Gross <jasongross9@gmail.com>
2020-10-15Consistent indentation + a few bullets in RIneq.v.Hugo Herbelin
2020-10-15Report a useful error for dependent destructionTej Chajed
Similar to `dependent induction`, report an error message for `dependent destruction` saying that importing `Coq.Program.Equality` is required, rather than failing at parsing time. This is a small extension of #605 to cover dependent destruction as well. Here I also put in some tests.
2020-10-11Modify ZArith/Znumtheory.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Zdiv.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Zcomplements.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/ZifyInst.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/ZifyClasses.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/Ztac.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/ZCoeff.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Zpow_def.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Wf_Z.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Zabs.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Znat.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/RingMicromega.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/Tauto.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/Refl.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/EnvRing.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify NArith/Ndigits.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify Strings/String.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify Strings/Ascii.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify Vectors/VectorEq.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify Vectors/VectorSpec.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify Vectors/VectorDef.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify Vectors/Fin.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/OrderedRing.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify Arith/Euclid.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify Arith/Div2.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify Arith/Even.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify setoid_ring/Ring.v to compile with -mangle-namesJasper Hugunin
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-06 19:22:05 +0000