Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge PR #6820: Tacticals assert_fails and assert_succeeds | Maxime Dénès | 2018-03-09 |
|\ | |||
* \ | Merge PR #6155: Get rid of ' notation for Zpos in QArith | Maxime Dénès | 2018-03-09 |
|\ \ | |||
* \ \ | Merge PR #6937: Add empty compat file for Coq 8.8 | Maxime Dénès | 2018-03-09 |
|\ \ \ | |||
* \ \ \ | Merge PR #6522: Fix core hint database issue #6521 | Maxime Dénès | 2018-03-08 |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #6743: Add notation {x & P} for sigT | Maxime Dénès | 2018-03-08 |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #6909: Deprecate Focus and Unfocus | Maxime Dénès | 2018-03-08 |
|\ \ \ \ \ \ | |||
* | | | | | | | [stdlib] Do not use “Require” inside sections | Vincent Laporte | 2018-03-07 |
| | | | | | | | |||
| | | | * | | | Add empty compat file for Coq 8.8 | Jason Gross | 2018-03-07 |
| |_|_|/ / / |/| | | | | | | | | | | | | | | | | | This closes #6598 | ||
* | | | | | | Merge PR #6744: Add String.concat | Maxime Dénès | 2018-03-07 |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #6855: Update headers following #6543. | Maxime Dénès | 2018-03-05 |
|\ \ \ \ \ \ \ | |||
| | | * | | | | | Remove all uses of Focus in standard library. | Théo Zimmermann | 2018-03-04 |
| | | | | | | | | |||
* | | | | | | | | Remove 8.5 compatibility support. | Théo Zimmermann | 2018-03-02 |
| | | | | | | | | |||
* | | | | | | | | Remove VOld compatibility flag. | Théo Zimmermann | 2018-03-02 |
| | | | | | | | | |||
* | | | | | | | | Turn warning for deprecated notations on. | Théo Zimmermann | 2018-03-02 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Fix new deprecation warnings in the standard library. | ||
* | | | | | | | | Remove the deprecation for some 8.2-8.5 compatibility aliases. | Théo Zimmermann | 2018-03-02 |
| |_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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. | ||
| | | | | | * | Uniform spacing layout in Tactics.v. | Hugo Herbelin | 2018-02-28 |
| | | | | | | | |||
| | | | | | * | Added tacticals assert_succeeds/assert_fails (courtesy of Jason Gross). | Hugo Herbelin | 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-28 |
|\ \ \ \ \ \ \ \ | |||
| | | * | | | | | | Update headers following #6543. | Théo Zimmermann | 2018-02-27 |
| |_|/ / / / / / |/| | | | | | | | |||
| | * | | | | | | [stdlib] move “Require” out of sections | Vincent Laporte | 2018-02-27 |
| |/ / / / / / |/| | | | | | | |||
| | * | | | | | Add String.concat | Jason Gross | 2018-02-24 |
| |/ / / / / |/| | | | | | |||
* | | | | | | Merge PR #6599: Decimals in prelude | Maxime Dénès | 2018-02-24 |
|\ \ \ \ \ \ | |_|_|_|_|/ |/| | | | | | |||
* | | | | | | Merge PR #6282: proposed fix for issue #3213: extra variable m in Lt.S_pred | Maxime Dénès | 2018-02-21 |
|\ \ \ \ \ \ | |||
| | * | | | | | Decimal goodies : conversion to/from Coq strings | Pierre Letouzey | 2018-02-20 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | Just because it's fun and easy. Not used by the Numeral Notation command. | ||
| | * | | | | | 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 | 2018-02-20 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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. | ||
* | | | | | | | 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-20 |
| |/ / / / / |/| | | | | | |||
* | | | | | | Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead. | Maxime Dénès | 2018-02-19 |
|\ \ \ \ \ \ | |||
| | | | * | | | Add notation {x & P} for sigT | Tej Chajed | 2018-02-12 |
| |_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | Analogous to existing `{x | P}` notation for `sig`, where the type of `x` is inferred instead of specified. | ||
* | | | | | | Merge PR #6139: Make list functions returning sumbools transparent | Maxime Dénès | 2018-02-12 |
|\ \ \ \ \ \ | |||
* | | | | | | | Document between and exists_between types. | Ismail | 2018-01-08 |
| | | | | | | | |||
| | * | | | | | Remove dir-locals and ship suggested helper hooks instead. | Gaëtan Gilbert | 2018-01-06 |
| |/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | .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. | ||
| | | | * | | Fix core hint database issue #6521 | Anton Trunov | 2018-01-03 |
| |_|_|/ / |/| | | | | |||
* | | | | | Fix warning about shadowing a global name. | Gaëtan Gilbert | 2017-12-19 |
| | | | | | |||
* | | | | | Add named timers to LtacProf | Jason Gross | 2017-12-14 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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. | ||
* | | | | | Merge PR #6335: Additional rewrite lemmas on Ensembles, in Powerset_facts | Maxime Dénès | 2017-12-12 |
|\ \ \ \ \ | |||
* | | | | | | Axiom-free proof of eta expansion. | Jasper Hugunin | 2017-12-11 |
| | | | | | | |||
* | | | | | | Remove most uses of function extensionality in Program.Combinators | Jasper Hugunin | 2017-12-09 |
| | | | | | | |||
| * | | | | | Additional rewrite lemmas on Ensembles, in Powerset_facts | Joachim Breitner | 2017-12-06 |
|/ / / / / | |||
| | * | | | proposed fix for issue #3213: extra variable m in Lt.S_pred | fredokun | 2017-12-01 |
| | | | | | |||
* | | | | | Fix (partial) #4878: option to stop autodeclaring axiom as instance. | Gaëtan Gilbert | 2017-11-28 |
| |/ / / |/| | | | |||
| * | | | Make list functions returning sumbools transparent | Tej Chajed | 2017-11-15 |
|/ / / | | | | | | | | | | Specifically Exists_dec, Forall_dec, and Forall_Exists_dec. | ||
| | * | Get rid of ' notation for Zpos in QArith. | Robbert Krebbers | 2017-11-14 |
| |/ |/| | |||
* | | 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-27 |
| | | | |||
| * | | Moving from `is_true` to `= true` | Raphaël Monat | 2017-10-25 |
| | | |