| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-06-10 | Tweak printing boxes for unicode binders | Ralf Jung | |
| 2018-06-05 | Merge PR #7690: Fixing typos in file Berardi.v | Pierre-Marie Pédrot | |
| 2018-06-04 | Deprecate implicit tactic solving. | Pierre-Marie Pédrot | |
| 2018-06-03 | Fixing typos in file Berardi.v | Hugo Herbelin | |
| Note that one of them is in the name of the main theorem, so we use a compatibility notation. | |||
| 2018-04-16 | Protecting against a "deprecated cofix" warning. | Hugo Herbelin | |
| 2018-04-13 | [ltac] Deprecate nameless fix/cofix. | Emilio Jesus Gallego Arias | |
| LTAC's `fix` and `cofix` do require access to the proof object inside the tactic monad when used without a name. This is a bit inconvenient as we aim to make the handling of the proof object purely functional. Alternatives have been discussed in #7196, and it seems that deprecating the nameless forms may have the best cost/benefit ratio, so opening this PR for discussion. See also #6171. | |||
| 2018-03-09 | 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-08 | 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-07 | [stdlib] Do not use “Require” inside sections | Vincent Laporte | |
| 2018-03-07 | Add empty compat file for Coq 8.8 | Jason Gross | |
| This closes #6598 | |||
| 2018-03-07 | Merge PR #6744: Add String.concat | Maxime Dénès | |
| 2018-03-05 | Merge PR #6855: Update headers following #6543. | Maxime Dénès | |
| 2018-03-04 | Remove all uses of Focus in standard library. | Théo Zimmermann | |
| 2018-03-02 | 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 | |
| Fix new deprecation warnings in the standard library. | |||
| 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 | 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-27 | Update headers following #6543. | Théo Zimmermann | |
| 2018-02-27 | [stdlib] move “Require” out of sections | Vincent Laporte | |
| 2018-02-24 | Add String.concat | Jason Gross | |
| 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 | Add notation {x & P} for sigT | Tej Chajed | |
| Analogous to existing `{x | P}` notation for `sig`, where the type of `x` is inferred instead of specified. | |||
| 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. | |||
| 2018-01-03 | Fix core hint database issue #6521 | Anton Trunov | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |