| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-02-20 | Decimal goodies : conversion to/from Coq strings | Pierre Letouzey | |
| Just because it's fun and easy. Not used by the Numeral Notation command. | |||
| 2018-02-20 | Decimal: proofs that conversions from/to nat,N,Z are bijections | Pierre Letouzey | |
| 2018-02-20 | Decimal: simple representation of base-10 numbers | Pierre Letouzey | |
| 2018-02-19 | Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead. | Maxime Dénès | |
| 2018-02-12 | Merge PR #6139: Make list functions returning sumbools transparent | Maxime Dénès | |
| 2018-01-08 | Document between and exists_between types. | Ismail | |
| 2018-01-06 | Remove dir-locals and ship suggested helper hooks instead. | Gaëtan Gilbert | |
| .dir-locals led to issues with unsafe local variable warnings. With this method the user is opting in to running this code so there are no warnings. | |||
| 2017-12-19 | Fix warning about shadowing a global name. | Gaëtan Gilbert | |
| 2017-12-14 | Add named timers to LtacProf | Jason Gross | |
| I'm not sure if they belong in profile_ltac, or in extratactics, or, perhaps, in a separate plugin. But I'd find it very useful to have a version of `time` that works on constr evaluation, which is what this commit provides. I'm not sure that I've picked good naming conventions for the tactics, either. | |||
| 2017-12-12 | Merge PR #6335: Additional rewrite lemmas on Ensembles, in Powerset_facts | Maxime Dénès | |
| 2017-12-11 | Axiom-free proof of eta expansion. | Jasper Hugunin | |
| 2017-12-09 | Remove most uses of function extensionality in Program.Combinators | Jasper Hugunin | |
| 2017-12-06 | Additional rewrite lemmas on Ensembles, in Powerset_facts | Joachim Breitner | |
| 2017-11-28 | Fix (partial) #4878: option to stop autodeclaring axiom as instance. | Gaëtan Gilbert | |
| 2017-11-15 | Make list functions returning sumbools transparent | Tej Chajed | |
| Specifically Exists_dec, Forall_dec, and Forall_Exists_dec. | |||
| 2017-10-27 | Merge PR #1113: Adding 3 Arith/QArith lemmas that I found useful | Maxime Dénès | |
| 2017-10-27 | Chaining two tactics in a proof | Raphaël Monat | |
| 2017-10-25 | Moving from `is_true` to `= true` | Raphaël Monat | |
| 2017-10-19 | Moving bug numbers to BZ# format in the source code. | Théo Zimmermann | |
| Compared to the original proposition (01f848d in #960), this commit only changes files containing bug numbers that are also PR numbers. | |||
| 2017-10-12 | Added proofs of Qeq_bool_refl, Qeq_bool_sym, Qeq_bool_trans. | Raphaël Monat | |
| 2017-10-10 | Merge PR #768: Omega and romega know about context definitions (fix old bug 148) | Maxime Dénès | |
| 2017-10-08 | Changed Qeq_bool_sym into Qeq_bool_comm, used the proof of @letouzey. | Raphaël Monat | |
| 2017-10-08 | Removed leb_not_le (already existing as Nat.leb_nle) | Raphaël Monat | |
| 2017-10-07 | Compat/Coq87.v : Unset Omega UseLocalDefs (see PR #768) | Pierre Letouzey | |
| 2017-10-05 | [ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms. | Emilio Jesus Gallego Arias | |
| The manual has long stated that these forms are deprecated. We add a warning for them, as indeed `Add Morphism` is an "proof evil" [*] command, and we may want to remove it in the future. We've also fixed the stdlib not to emit the warning. [*] https://ncatlab.org/nlab/show/principle+of+equivalence | |||
| 2017-10-03 | Changed the statement of leb_not_le; shortened the proof | Raphaël Monat | |
| 2017-10-03 | Add Qabs_Qinv: Qabs (/ q) == / (Qabs q). | Raphaël Monat | |
| 2017-10-03 | Add Qeq_bool_sym: Qeq_bool x y = Qeq_bool y x. | Raphaël Monat | |
| 2017-10-03 | Add leb_not_le: (n <=? m) = false -> n > m. | Raphaël Monat | |
| 2017-09-15 | Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" ↵ | Maxime Dénès | |
| work better on them | |||
| 2017-09-03 | Addressing BZ#5713 (classical_left/classical_right artificially restricted). | Hugo Herbelin | |
| As explained in BZ#5713 report, the requirement for a non-empty context is not needed, so we remove it. | |||
| 2017-08-29 | A little reorganization of notations + a fix to #5608. | Hugo Herbelin | |
| - Formerly, notations such as "{ A } + { B }" were typically split into "{ _ }" and "_ + _". We keep the split only for parsing, which is where it is really needed, but not anymore for interpretation, nor printing. - As a consequence, one notation string can give rise to several grammar entries, but still only one printing entry. - As another consequence, "{ A } + { B }" and "A + { B }" must be reserved to be used, which is after all the natural expectation, even if the sublevels are constrained. - We also now keep the information "is ident", "is binder" in the "key" characterizing the level of a notation. | |||
| 2017-08-21 | Ensuring all .v files end with a newline to make "sed -i" work better on them. | Hugo Herbelin | |
| 2017-07-26 | Merge PR #882: Adding a V8.7 compatibility version number. | Maxime Dénès | |
| 2017-07-26 | Merge PR #885: Removing a dummy parameter in some FMapPositive statements. | Maxime Dénès | |
| 2017-07-26 | Merge PR #845: Add Z.mod_div lemma to standard library. | Maxime Dénès | |
| 2017-07-21 | Adding a V8.7 compatibility version number. | Hugo Herbelin | |
| 2017-07-16 | Removing a dummy parameter in some FMapPositive statements. | Hugo Herbelin | |
| The statements xelements_bits_lt_1 and xelements_bits_lt_2 had an unexpected extra dependency due to a name collision with a section variable. | |||
| 2017-07-05 | Fix typo in documentation for identity | Tej Chajed | |
| Fixes Coq bug 5635 (https://coq.inria.fr/bugs/show_bug.cgi?id=5635). | |||
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot | |
| 2017-06-29 | Fix Zmod_div. | Russell O'Connor | |
| 2017-06-29 | Use forall for consistency | roconnor-blockstream | |
| 2017-06-29 | Add Z.mod_div lemma to standard library. | Russell O'Connor | |
| 2017-06-26 | Merge PR#826: Put plugin exports in the right compatibility file | Maxime Dénès | |
| 2017-06-23 | Merge PR#794: Cleanup of ltac cmxs | Maxime Dénès | |
| 2017-06-22 | Put plugin exports in the right compatibility file | Jason Gross | |
| This closes [bug #5607](https://coq.inria.fr/bugs/show_bug.cgi?id=5607). PR #220 put the exports in the wrong compat files, presumably because it was originally targeted to version 8.6, and this wasn't updated when it was retargeted to version 8.7. | |||
| 2017-06-15 | plugins/ltac : avoid spurious .cmxs files | Pierre Letouzey | |
| In the previous setting, all plugins/ltac/*.cmxs except ltac_plugin.cmxs (for instance coretactics.cmxs, g_auto.cmxs, ...) were utterly bogus : - wrong -for-pack used for their inner .cmx - dependency over modules not provided (for instance Tacenv, that ends up being a submodule of the pack ltac_plugin). But we were lucky, those files were actually never loaded, thanks to the several DECLARE PLUGIN inside coretactics and co, that end up in ltac_plugin, and hence tell Coq that these modules are already known, preventing any attempt to load them. Anyway, this commit cleans up this mess (thanks PMP for the help) | |||
| 2017-06-15 | Merge PR#375: Deprecation | Maxime Dénès | |
| 2017-06-14 | Merge PR#753: Fix bug 5026 (the stdlib shouldn't define inconsistent notations). | Maxime Dénès | |
| 2017-06-14 | Prelude : no more autoload of plugins extraction and recdef | Pierre Letouzey | |
| The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |