| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-07-10 | Fix typo in Init.Logic. | whitequark | |
| 2018-07-02 | hints: add Hint Variables/Constants Opaque/Transparent commands | Matthieu Sozeau | |
| This gives user control on the transparent state of a hint db. Can override defaults more easily (report by J. H. Jourdan). For "core", declare that variables can be unfolded, but no constants (ensures compatibility with previous auto which allowed conv on closed terms) Document Hint Variables | |||
| 2018-06-29 | Splitting primitive numeral parser/printer for positive, N, Z into three files. | Hugo Herbelin | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |