aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
2020-04-01[micromega] use Coqlib.lib_ref to get Coq constants.Frédéric Besson
2020-03-31NArith, PArith: Add facts about iterLysxia
2020-03-30Merge PR #11725: Cleanup stdlib reals.Hugo Herbelin
Ack-by: SkySkimmer Reviewed-by: herbelin
2020-03-30Missing apartness notationsVincent Semeria
2020-03-30new sig notations and spaces addedOlivier Laurent
2020-03-30Merge PR #11018: “auto with zarith”: use “lia” rather than “omega”Maxime Dénès
Ack-by: Zimmi48 Reviewed-by: anton-trunov Ack-by: jfehrle Reviewed-by: maximedenes
2020-03-28Remove SearchAbout command, deprecated in 8.5Jim Fehrle
2020-03-27Cleanup stdlib reals. Use implicit arguments for ConstructiveReals. Move ↵Vincent Semeria
ConstructiveReals into new directory Abstract. Remove imports of implementations inside those Abstract files. Add changelog for constructive reals cleanup Move Cauchy reals into new directory Cauchy Update stdlib index Rename sum_f_R0 Use coqdoc comments Update doc/changelog/10-standard-library/11725-cleanup-reals.rst Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com> Update doc/changelog/10-standard-library/11725-cleanup-reals.rst Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com> Update doc/changelog/10-standard-library/11725-cleanup-reals.rst Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com> Improve notations
2020-03-27Merge PR #11848: Nicer printing for decimal constantsHugo Herbelin
Reviewed-by: herbelin
2020-03-26Merge PR #11885: Sorting: Swap the names of Sorted_sort and LocallySorted_sortHugo Herbelin
Reviewed-by: herbelin
2020-03-25Make the level of ≡ in Int63 consistent with =Jason Gross
Fixes #11905
2020-03-25Nicer printing for decimal constants in QPierre Roux
Print 1.5 as 1.5 and not 15e-1. We choose the shortest representation with tie break to the dot notation (0.01 rather than 1e-3). The printing remains injective, i.e. 12/10 is not mixed with 120/100, the first being printed as 1.2 and the last as 1.20.
2020-03-24“auto with zarith”: use “lia” rather than “omega”Vincent Laporte
2020-03-24[stdlib] Do not rely on failing “auto”Vincent Laporte
2020-03-23Fix levels of `<=?` and `<?` in the stdlibJason Gross
They were defined at level 70, no associativity in all but three places, where they were instead declared at level 35. Fixes #11890
2020-03-23Sorting: Swap the names of Sorted_sort and LocallySorted_sortLysxia
2020-03-21Add module ZifyPow to avoid compatibility issue with 8.11.Théo Zimmermann
Also tweak the changelog entry to explain the difference.
2020-03-19Merge PR #11760: firstorder: default tactic is “auto with core”Théo Zimmermann
Reviewed-by: JasonGross Reviewed-by: Zimmi48
2020-03-19Merge PR #11822: Grants #11692: clear dependent knows about let-inPierre-Marie Pédrot
Reviewed-by: JasonGross Reviewed-by: ppedrot
2020-03-19firstorder: default tactic is “auto with core”Vincent Laporte
2020-03-19[stdlib] Remove a few `auto with *`Vincent Laporte
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2020-03-18Merge PR #11746: Register commonly used names from the Reals library for ↵Théo Zimmermann
plugins (e.g. gappa) Reviewed-by: Zimmi48
2020-03-14Fixes #11692 (clear dependent knows about let-in).Hugo Herbelin
2020-03-06Fix #11738 : Funind using deprecated Coqlib API.Pierre Courtieu
2020-03-04Add file to register names of reals library used by gappaMichael Soegtrop
2020-03-03[zify] efficiency improvementsFrédéric Besson
- zify_iter_specs is entirely in OCaml - zify_op has been improved * The generation of proof-terms is more direct * It does not `rewrite` but instead either performs a `pose proof` or a `change` * The support for `and`, `or`, `not`, arrow is hardcoded * Avoid generating duplicate hypotheses such as 0 <= Z.of_nat x - zify_elim_let is entirely in OCaml (no Ltac callback) [micromega] fix stack overflow Less naive computation of bounds (online elimination of duplicates)
2020-02-26Merge PR #11644: Use implicit arguments in notations for eq.Hugo Herbelin
Reviewed-by: herbelin
2020-02-26Consolidate int63-related notationsMaxime Dénès
We avoid redundant notations for the same concepts and make sure notations do not break Ltac parsing for users of these libraries.
2020-02-25Use implicit arguments in notations for eq.Gaëtan Gilbert
This gives IMO slightly nicer errors when the type cannot be inferred, ie ~~~coq Type (forall x, x = x). ~~~ says "cannot infer the implicit parameter A of eq" instead of "cannot infer this placeholder".
2020-02-19Only parsing in Reserved Notation: turning notice into a warning.Hugo Herbelin
2020-02-19Choosing a standard format for the "rew dependent" notation.Hugo Herbelin
2020-02-18Merge PR #11529: [build] Consolidate stdlib's .v files under a single directory.Théo Zimmermann
Reviewed-by: Zimmi48
2020-02-17Merge PR #11350: stdlib List: add [remove'] and [count_occ'] that use [filter]Hugo Herbelin
Reviewed-by: anton-trunov
2020-02-13[build] Consolidate stdlib's .v files under a single directory.Emilio Jesus Gallego Arias
Currently, `.v` under the `Coq.` prefix are found in both `theories` and `plugins`. Usually these two directories are merged by special loadpath code that allows double-binding of the prefix. This adds some complexity to the build and loadpath system; and in particular, it prevents from handling the `Coq.*` prefix in the simple, `-R theories Coq` standard way. We thus move all `.v` files to theories, leaving `plugins` as an OCaml-only directory, and modify accordingly the loadpath / build infrastructure. Note that in general `plugins/foo/Foo.v` was not self-contained, in the sense that it depended on files in `theories` and files in `theories` depended on it; moreover, Coq saw all these files as belonging to the same namespace so it didn't really care where they lived. This could also imply a performance gain as we now effectively traverse less directories when locating a library. See also discussion in #10003
2020-02-08Remove -compat 8.9.Théo Zimmermann
Commit auto-generated by running dev/tools/update-compat.py --release. As per release doc this must be run at some point before branching (not necessarily close to the branching date).
2020-02-08Merge PR #11240: Add rew dependent NotationsHugo Herbelin
Reviewed-by: herbelin Ack-by: jfehrle
2020-02-06replace RList by list RYves Bertot
add an overlay for coquelicot remove functions from RList: In, Rlength, cons_Rlist, app_RList because they are essentially the same as In, length, app, and map from List (beware that the order of arguments changes for map, and the In function contains reversed equalities). adds deprecation warnings for Rlist and Rlength adds deprecated notations for RList.cons and RList.nil
2020-01-17Fix issue #11396 : Rlist hides standard list constructors cons and nilMichael Soegtrop
2020-01-14Merge PR #11249: [stdlib] Additional statements in List.vHugo Herbelin
Reviewed-by: anton-trunov Reviewed-by: herbelin
2020-01-08Avoid hardcoded paths in extractionMaxime Dénès
2020-01-06stdlib List: add [remove'] and [count_occ']Yishuai Li
2020-01-05apply suggestions of @anton-trunovOlivier Laurent
2020-01-05clean some indentationsOlivier Laurent
2019-12-26Add rew dependent NotationsJason Gross
This way when users `Import EqNotations`, we get pretty-printing for equality `match` statements too.
2019-12-24Add statements with output in TypeOlivier Laurent
2019-12-23Merge PR #10760: Make rapply handle all numbers of underscoresPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2019-12-17[micromega] fix efficiency regressionFrédéric Besson
PR #9725 fixes completness bugs introduces some inefficiency. The current PR intends to fix the inefficiency while retaining completness. The fix removes a pre-processing step and instead relies on a more elaborate proof format introducing positivity constraints on the fly. Solve bootstrapping issues: RMicromega <-> Rbase <-> lia. Fixes #11063 and fixes #11242 and fixes #11270
2019-12-14Being explicit on existence of a remote link.Hugo Herbelin
2019-12-06Merge PR #11127: Added theorem Nat.bezout_comm.Hugo Herbelin
Ack-by: Zimmi48 Ack-by: herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-07 21:12:12 +0000