| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-10-10 | Merge PR #768: Omega and romega know about context definitions (fix old bug 148) | Maxime Dénès | |
| 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-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. | |||
| 2017-06-14 | Remove deprecated options from the standard library. | Guillaume Melquiond | |
| 2017-06-14 | Remove support for Coq 8.4. | Guillaume Melquiond | |
| 2017-06-14 | Merge PR#498: Bignums as a separate opam package | Maxime Dénès | |
| 2017-06-13 | Merge PR#385: Equality of sigma types | Maxime Dénès | |
| 2017-06-13 | BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo) | Pierre Letouzey | |
| See now https://github.com/coq/bignums Int31 is still in the stdlib. Some proofs there has be adapted to avoid the need for BigNumPrelude. | |||
| 2017-06-10 | Remove remaining vo.itarget files (obsolete since PR #499) | Pierre Letouzey | |
| 2017-06-08 | Fix bug 5026 (the stdlib shouldn't define inconsistent notations). | Théo Zimmermann | |
| 2017-06-01 | drop vo.itarget files and compute the corresponding the corresponding values ↵ | Matej Kosik | |
| automatically instead | |||
| 2017-05-28 | More uniform indentation of sigma lemmas | Jason Gross | |
| 2017-05-28 | Give explicit proof terms to proj2_sig_eq etc. | Jason Gross | |
| 2017-05-28 | Use the rew dependent notation in ex, ex2 proofs | Jason Gross | |
| 2017-05-28 | Make theorems about ex equality Qed | Jason Gross | |
| As requested in https://github.com/coq/coq/pull/384#issuecomment-303809461 | |||
| 2017-05-28 | Make new proofs of equality Qed | Jason Gross | |
| As requested in https://github.com/coq/coq/pull/384#issuecomment-303809461 | |||
| 2017-05-28 | Add some more comments about sigma equalities | Jason Gross | |
| Forwards/backwards reasoning thoughts come from https://github.com/coq/coq/pull/385#discussion_r111008347 | |||
| 2017-05-28 | Remove motive argument from [rew dependent] | Jason Gross | |
| 2017-05-28 | Use a local [rew dependent] notation | Jason Gross | |
| 2017-05-28 | Add forward-chaining versions: [eq_sig*_uncurried] | Jason Gross | |
| 2017-05-28 | Use notation for sigT | Jason Gross | |
| 2017-05-28 | Remove reference to [IsIso] | Jason Gross | |
| 2017-05-28 | Use notations for [sig], [sigT], [sig2], [sigT2] | Jason Gross | |
| 2017-05-28 | Use extended notation for ex, ex2 types | Jason Gross | |
| 2017-05-28 | Replace [ex'] with [ex] | Jason Gross | |
| The ' was originally denoting that we were taking in the projections and applying the constructor in the conclusion, rather than taking in the bundled versions and projecting them out (because the projections don't exist for [ex] and [ex2]). But we don't have versions like this for [sig] and [sigT] and [sigT2] and [sig2], so we might as well not add the ' to the [ex] and [ex2] versions. | |||
| 2017-05-28 | Use [rew_] instead of [eq_rect_] prefix | Jason Gross | |
| As per Hugo's request. | |||
| 2017-05-28 | Add equality lemmas for sig2 and sigT2 | Jason Gross | |
| 2017-05-28 | Add lemmas for ex2 | Jason Gross | |
| 2017-05-28 | Use [rew] notations rather than [eq_rect] | Jason Gross | |
| As per Hugo's suggestion in https://github.com/coq/coq/pull/384#issuecomment-264891011 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |