| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-03-02 | Remove the deprecation for some 8.2-8.5 compatibility aliases. | Théo Zimmermann | |
| This was decided during the Fall WG (2017). The aliases that are kept as deprecated are the ones where the difference is only a prefix becoming a qualified module name. The intention is to turn the warning for deprecated notations on. We change the compat version to 8.6 to allow the removal of VOld and V8_5. | |||
| 2018-02-28 | Merge PR #6852: [stdlib] move “Require” out of sections | Maxime Dénès | |
| 2018-02-28 | Merge PR #1026: changed statements of Rpower_lt and Rle_power and added lemmas | Maxime Dénès | |
| 2018-02-27 | [stdlib] move “Require” out of sections | Vincent Laporte | |
| 2018-02-24 | Merge PR #6599: Decimals in prelude | Maxime Dénès | |
| 2018-02-21 | Merge PR #6282: proposed fix for issue #3213: extra variable m in Lt.S_pred | Maxime Dénès | |
| 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-20 | Trying a hack to support {'pat|P} without breaking compatibility. | Hugo Herbelin | |
| Concretely, we bypass the following limitation: The notation "{ ' pat | P }" broke the parsing of expressions of the form "{ forall x, P } + { Q }". Indeed the latter works thanks to a tolerance of Camlp5 in parsing "forall x, P" at level 200 while the rule asks to actually parse the interior of "{ ... }" at level 99 (the reason for 99 is to be below the rule for "M : T" which is at level 100, so that "{ x : A | P }" does not see "x : A" as a cast). Adding an extra "'"; pat = pattern in parallel to c = constr LEVEL "99" broke the tolerance for constr at level 200. We fix this by adding an ad hoc rule for "{ binder_constr }" in the native grammar (g_constr.ml4). Actually, this is inconsistent with having a rule for "{ constr at level 99 }" in Notations.v. We should have both rules in Notations.v or both rules hard-wired in the native grammar. But I still don't know what is the best decision to take, so leaving as it at the current time. Advantages of hard-wiring both rules in g_constr.ml4: a bit simpler in metasyntax.ml (no need to ensure that the rule exist). Disadvantages: if one wants a different initial state without the business needing the "{ }" for sumbool, sumor, sig, sigT, one still have the rules there. Advantages of having them in Notations.v: more modular, we can change the initial state. Disadvantages: one would need a new kind of modifier, something like "x at level 99 || binder_constr", with all the difficulty to find a nice, intuitive, name for "binder_constr", and the difficulty of understanding if there is a generality to this "||" disjunction operator, and whether it should be documented or not. | |||
| 2018-02-20 | Adding notations of the form "{'pat|P}", "exists2 'pat, P & Q", etc. | Hugo Herbelin | |
| 2018-02-20 | More structured printing in unicode notations for binders. | Hugo Herbelin | |
| 2018-02-20 | User-level support for Gonthier-Ssreflect's "if t then pat then u else v". | Hugo Herbelin | |
| 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-12-01 | proposed fix for issue #3213: extra variable m in Lt.S_pred | fredokun | |
| 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-06 | weakens an hypothesis of Rle_Rpower | Yves Bertot | |
| 2017-09-06 | changed statements of Rpower_lt and Rle_power and added | Yves Bertot | |
| Rlt_Rpower_l and pow_INR. Unfortunately theorems Rpower_lt and Rle_power are named inconsistently, in spite of their similarity. | |||
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |