aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
2021-04-23Merge PR #14041: Enable canonical fun _ => _ projections.coqbot-app[bot]
Reviewed-by: gares Ack-by: Janno Ack-by: CohenCyril Ack-by: Zimmi48 Ack-by: jfehrle Ack-by: SkySkimmer
2021-04-22Enable canonical `fun _ => _` projections.Jan-Oliver Kaiser
2021-04-21Merge PR #13911: Remove the :> type cast?coqbot-app[bot]
Reviewed-by: mattam82 Ack-by: Zimmi48
2021-04-19Merge PR #14108: [zify] bugfixVincent Laporte
Reviewed-by: Zimmi48 Reviewed-by: vbgl
2021-04-16[zify] bugfixFrederic Besson
- to zify the conclusion, we are using Tactics.apply (not rewrite) Closes #11089 - constrain the arguments of Add Zify X to be GlobRef.t Unset Primitive Projections so that projections are GlobRef.t. Closes #14043 Update doc/sphinx/addendum/micromega.rst Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2021-04-12[zify] More aggressive application of saturation rulesBESSON Frederic
The role of the `zify_saturate` tactic is to augment the goal with positivity constraints. The premisses were previously obtained from the context. If they are not present, we instantiate the saturation lemma anyway. Also, - Remove saturation rules for Z.mul, the reasoning is performed by lia/nia - Run zify_saturate after zify_to_euclidean_division_equations - Better lemma for Z.power - Ensure that lemma are generated once Co-authored-by: Andrej Dudenhefner <mrhaandi> Closes #12184, #11656
2021-04-12Merge PR #14061: [zify] better error reportingVincent Laporte
Reviewed-by: vbgl
2021-04-12[zify] better error reportingBESSON Frederic
The vernacular command takes a reference instead of a constr. Moreover, the head symbol is checked i.e Add Zify InjTyp ref checks that the referenced term has type Intyp X1 ... Xn Closes #14054, #13242 Co-authored-by: Vincent Laporte <vbgl@users.noreply.github.com>
2021-04-07Merge PR #14056: Miscellaneous mini-"typos" fixescoqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: jfehrle Reviewed-by: silene
2021-04-07Merge PR #14008: [stdlib] [Arith] Cantor pairingcoqbot-app[bot]
Reviewed-by: olaure01 Ack-by: jfehrle
2021-04-06Merge PR #14077: Add odoc warnings for empty packages.coqbot-app[bot]
Reviewed-by: ejgallego
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
From an OCaml library point of view.
2021-04-02Remove the omega tactic and related optionsJim Fehrle
2021-04-02add Cantor pairing to_nat and its inverse of_natAndrej Dudenhefner
add polynomial specifications of to_nat add changelog and doc entries
2021-03-31Merge PR #14022: Replace mentions of Num by Zarith.coqbot-app[bot]
Reviewed-by: pi8027
2021-03-30Remove the :> type castJim Fehrle
2021-03-28Replace mentions of Num by Zarith.Guillaume Melquiond
The documentation of extraction became outdated when the big.ml wrapper got modified by 094e4649c29e2426daca0476c140439de901dafe.
2021-03-26remove in List.v deprecated/unnecessary dependencies: Le, Gt, Minus, Lt, SetoidAndrej Dudenhefner
fix unexpectedly broken MSetGenTree.v add changelog entry
2021-03-23add lemmas to List.v: Exists_map, Exists_concat, Exists_flat_map, ↵Andrej Dudenhefner
Forall_map, Forall_concat, Forall_flat_map, nth_error_map, nth_repeat, nth_error_repeat
2021-03-23Merge PR #13671: [stdlib] [Vectors] add results on to_listcoqbot-app[bot]
Reviewed-by: anton-trunov
2021-03-23Merge PR #13804: [stdlib] [List] Add results about count_occcoqbot-app[bot]
Reviewed-by: anton-trunov
2021-03-19Merge PR #13730: Lint stdlib with -mangle-names #6coqbot-app[bot]
Reviewed-by: anton-trunov
2021-03-16add results on to_listOlivier Laurent
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
We introduce a new package structure for Coq: - `coq-core`: Coq's OCaml tools code and plugins - `coq-stdlib`: Coq's stdlib [.vo files] - `coq`: meta-package that pulls `coq-{core,stdlib}` This has several advantages, in particular it allows to install Coq without the stdlib which is useful in several scenarios, it also open the door towards a versioning of the stdlib at the package level. The main user-visible change is that Coq's ML development files now live in `$lib/coq-core`, for compatibility in the regular build we install a symlink and support both setups for a while. Note that plugin developers and even `coq_makefile` should actually rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust. There is a transient state where we actually look for both `$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support the non-ocamlfind plus custom variables. This will be much improved once #13617 is merged (which requires this PR first), then, we will introduce a `coq.boot` library so finally `coqdep`, `coqchk`, etc... can share the same path setup code. IMHO the plan should work fine.
2021-02-26Signed primitive integersAna
Signed primitive integers defined on top of the existing unsigned ones with two's complement. The module Sint63 includes the theory of signed primitive integers that differs from the unsigned case. Additions to the kernel: les (signed <=), lts (signed <), compares (signed compare), divs (signed division), rems (signed remainder), asr (arithmetic shift right) (The s suffix is not used when importing the Sint63 module.) The printing and parsing of primitive ints was updated and the int63_syntax_plugin was removed (we use Number Notation instead). A primitive int is parsed / printed as unsigned or signed depending on the scope. In the default (Set Printing All) case, it is printed in hexadecimal.
2021-02-25Merge PR #13080: Ascii: add leb and ltbcoqbot-app[bot]
Reviewed-by: anton-trunov
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
The function returned by DRealAbstr starts by a call to the axiom sig_forall_dec, so it is not computable anyway.
2021-02-19Terminate some lemmas with Qed.Guillaume Melquiond
Since the proofs start by applying or destructuring Qed-ed lemmas, they cannot be used in a computational setting, so no need for them to be Defined.
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]
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2021-01-25Remove the Hide Obligations flagJim Fehrle
2021-01-20Use cbn instead of simpl in a proof of HexadecimalNat.Pierre-Marie Pédrot
This reduces the tactic invocation time from 10s to 0.25s on my machine. I was growing tired of having to wait for that file while compiling the stdlib.
2021-01-19Merge PR #13699: Fix #13579 (hnf on primitives raises an anomaly)Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
We deprecate unspecified locality as was done for Hint. Close #13724
2021-01-18Fix #13579 (hnf on primitives raises an anomaly)Pierre Roux
Also works for simpl.
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
I used `match goal` a lot to access hypotheses without knowing their name.
2021-01-08Modify Sorting/Sorted.v to compile with -mangle-namesJasper Hugunin
2021-01-08Modify Classes/EquivDec.v to compile with -mangle-namesJasper Hugunin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:38:48 +0000