aboutsummaryrefslogtreecommitdiff
path: root/theories/ZArith
AgeCommit message (Collapse)Author
2021-04-02Remove the omega tactic and related optionsJim Fehrle
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
We deprecate unspecified locality as was done for Hint. Close #13724
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-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
By default Coq stdlib warnings raise an error, so this is really required.
2020-11-09Merge PR #13173: Lint stdlib with -mangle-names #4coqbot-app[bot]
Reviewed-by: anton-trunov
2020-11-05Rename Dec and HexDec to Decimal and HexadecimalPierre Roux
As noted by Hugo Herbelin, Dec is rather used for "decidable".
2020-10-30Renaming Numeral.v into Number.vPierre Roux
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 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-09Modify ZArith/ZArith_dec.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify ZArith/Zorder.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify ZArith/BinInt.v to compile with -mangle-namesJasper Hugunin
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
Keep Numeral Notation wit a deprecation warning.
2020-06-14[micromega] native support for boolean operatorsFrédéric Besson
The syntax of formulae is extended to support boolean constants (true, false), boolean operators Bool.andb, Bool.orb, Bool.implb, Bool.negb, Bool.eqb and comparison operators Z.eqb, Z.ltb, Z.gtb, Z.leb and Z.ltb.
2020-05-09Add hexadecimal numeralsPierre Roux
We add hexadecimal numerals according to the following regexp 0[xX][0-9a-fA-F][0-9a-fA-F_]*(\.[0-9a-fA-F_]+)?([pP][+-]?[0-9][0-9_]*)? This is unfortunately a rather large commit. I suggest reading it in the following order: * test-suite/output/ZSyntax.{v,out} new test * test-suite/output/Int63Syntax.{v,out} '' * test-suite/output/QArithSyntax.{v,out} '' * test-suite/output/RealSyntax.{v,out} '' * test-suite/output/FloatSyntax.{v,out} '' * interp/numTok.ml{i,} extending numeral tokens * theories/Init/Hexadecimal.v adaptation of Decimal.v for the new hexadecimal Numeral Notation * theories/Init/Numeral.v new interface for Numeral Notation (basically, a numeral is either a decimal or an hexadecimal) * theories/Init/Nat.v add hexadecimal numeral notation to nat * theories/PArith/BinPosDef.v '' positive * theories/ZArith/BinIntDef.v '' Z * theories/NArith/BinNatDef.v '' N * theories/QArith/QArith_base.v '' Q * interp/notation.ml{i,} adapting implementation of numeral notations * plugins/syntax/numeral.ml '' * plugins/syntax/r_syntax.ml adapt parser for real numbers * plugins/syntax/float_syntax.ml adapt parser for primitive floats * theories/Init/Prelude.v register parser for nat * adapting the test-suite (test-suite/output/NumeralNotations.{v,out} and test-suite/output/SearchPattern.out) * remaining ml files (interp/constrex{tern,pr_ops}.ml where two open had to be permuted)
2020-05-09Merge PR #11990: [micromega] use Coqlib.lib_ref to get Coq constants.Maxime Dénès
Reviewed-by: maximedenes
2020-05-01Fixing #11903: Fixpoints not truly recursive in standard library.Hugo Herbelin
There was also a non truly recursive in the doc.
2020-04-01[micromega] use Coqlib.lib_ref to get Coq constants.Frédéric Besson
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2019-10-31Zdigits: use “lia” rather than “omega”Vincent Laporte
2019-10-31Zquot: use “lia” rather than “omega”Vincent Laporte
2019-10-31Zpow_facts: use “lia” rather than “omega”Vincent Laporte
2019-10-31Zwf: use “lia” rather than “omega”Vincent Laporte
2019-10-31Zgcd_alt: use “lia” rather than “omega”Vincent Laporte
2019-10-22Zpower: do not use “omega”Vincent Laporte
2019-10-22Znumtheory: do not use “omega”Vincent Laporte
2019-10-22Zdiv: do not use “omega”Vincent Laporte
2019-10-22Zcomplements: do not use “omega”Vincent Laporte
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
This could be Prop (for compat with usual Coq), Set (for HoTT), or actually an arbitrary "i". Take lower bound of universes into account in pretyping/engine Reinstate proper elaboration of SProp <= l constraints: replacing is_small with equality with lbound is _not_ semantics preserving! lbound = Set Elaborate template polymorphic inductives with lower bound Prop This will make more constraints explicit Check univ constraints with Prop as lower bound for template inductives Restrict template polymorphic universes to those not bounded from below Fixes #9294 fix suggested by Matthieu Try second fix suggested by Matthieu Take care of modifying elaboration for record declarations as well. Rebase and export functions for debug Remove exported functions used while debugging Add a new typing flag "check_template" and option "-no-template-checl" This parameterizes the new criterion on template polymorphic inductives to allow bypassing it (necessary for backward compatibility). Update checker to the new typing flags structure Switch on the new template_check flag to allow old unsafe behavior in indTyping. This is the only change of code really impacting the kernel, together with the commit implementing unbounded from below and parameterization by the lower bound on universes. Add deprecated option `Unset Template Check` allowing to make proof scripts work with both 8.9 and 8.10 for a while Fix `Template Check` option name and test it Add `Unset Template Check` to Coq89.v Cooking of inductives and template-check tests Cleanup test-suite file for template check / universes(template) flags cookind tests Move test of `Unset Template Check` to the failure/ dir, but comment it for now Template test-suite test explanation Overlays for PR 9918 Overlay for paramcoq Add overlay for fiat_parsers (-no-template-check) Add overlay for fiat_crypto_legacy Update fiat-crypto legacy overlay Now it points at the version that I plan on merging; I am hoping that doing this will guard against mistakes by adding an extra check that the target tested by Coq's CI on this branch works with the change I made. Remove overlay that should no longer be necessary The setting in the compat file should handle it Remove now-merged fiat-crypto-legacy overlay Update `Print Assumptions` to reflect the typing flag for template checking Fix About and Print Assumptions for template poly, giving info on which variables are actually polymorphic Fix pretty printing to print global universe levels properly Fix printing of template polymorphic universes Fix pretty printing for template polymorphism on no universe Fix interaction of template check and universes(template) flag Fix indTyping to really check if there is any point in polymorphism: the conclusion sort should be parameterized over at least one local universe Indtyping fixes for template polymorphic Props Allow explicit template polymorphism again Adapt to new indTyping interface Handle the case of template-polymorphic on no universes correctly (morally Type0m univ represented as Prop). Fix check of meaningfullness of template polymorphism in the kernel. It is now done w.r.t the min_univ, the minimal universe inferred for the inductive/record type, independently of the user-written annotation which must only be larger than min_univ. This preserves compatibility with UniMath and template-polymorphism as it has been implemented up-to now. Comment on identity non-template-polymorphism Remove incorrect universes(template) attributes from ssr simpl_fun can be meaningfully template-poly, as well as pred_key (although the use is debatable: it could just as well be in Prop). Move `fun_of_simpl` coercion declaration out of section to respect uniform inheritance Remove incorrect uses of #[universes(template)] from the stdlib Extraction of micromega changes due to moving an ind decl out of a section Remove incorrect uses of #[universes(template)] from plugins Fix test-suite files, removing incorrect #[universes(template)] attributes Remove incorrect #[universes(template)] attributes in test-suite Fix test-suite Remove overlays as they have been merged upstream.
2019-07-26[stdlib] Remove deprecated module Zsqrt_compatVincent Laporte
2019-07-26[stdlib] Remove deprecated module ZlogarithmVincent Laporte
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-23Fixing typos - Part 3JPR
2019-04-02Remove -compat 8.7Jason Gross
This removes various compatibility notations. Closes #8374 This commit was mostly created by running `./dev/tools/update-compat.py --release`. There's a bit of manual spacing adjustment around all of the removed compatibility notations, and some test-suite updates were done manually. The update to CHANGES.md was manual.
2019-03-14BinInt: 3 lemmas about testbit, mod _ 2^, onesAndres Erbsen
2018-12-19Put #[universes(template)] on all auto template spots in stdlibGaëtan Gilbert
2018-11-14Deprecate hint declaration/removal with no specified databaseMaxime Dénès
Previously, hints added without a specified database where implicitly put in the "core" database, which was discouraged by the user manual (because of the lack of modularity of this approach).
2018-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
We refactor the `Coqlib` API to locate objects over a namespace `module.object.property`. This introduces the vernacular command `Register g as n` to expose the Coq constant `g` under the name `n` (through the `register_ref` function). The constant can then be dynamically located using the `lib_ref` function. Co-authored-by: Emilio Jesús Gallego Arias <e+git@x80.org> Co-authored-by: Maxime Dénès <mail@maximedenes.fr> Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
2018-10-02Update compat notations to be compat 8.7Jason Gross
All changes done with ``` git grep --name-only 'compat "8.6"' | xargs sed -i s'/compat "8.6"/compat "8.7"/g' ``` As per https://github.com/coq/coq/pull/8374#issuecomment-426202818 and https://github.com/coq/coq/issues/8383#issuecomment-426200497
2018-09-11Merge PR #8425: Deprecate romega in favor of liaPierre-Marie Pédrot
2018-09-10Adapting standard library to the introduction of "Declare Scope".Hugo Herbelin
Removing in passing two Local which are no-ops in practice.
2018-09-10Deprecate romega in favor of lia.Vincent Laporte
2018-08-31Make Numeral Notation follow Import, not RequireJason Gross
Because that's the sane thing to do. This will inevitably cause issues for projects which do not `Import Coq.Strings.Ascii` before trying to use ascii notations. We also move the syntax plugin for `int31` notations from `Cyclic31` to `Int31`, so that users (like CompCert) who merely `Require Import Coq.Numbers.Cyclic.Int31.Int31` get the `int31` numeral syntax. Since `Cyclic31` `Export`s `Int31`, this should not cause any additional incompatibilities.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:00:21 +0000