aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Collapse)AuthorAge
* Fix typo in Init.Logic.Gravatar whitequark2018-07-10
|
* hints: add Hint Variables/Constants Opaque/Transparent commandsGravatar Matthieu Sozeau2018-07-02
| | | | | | | | | | | 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
* Splitting primitive numeral parser/printer for positive, N, Z into three files.Gravatar Hugo Herbelin2018-06-29
|
* Tweak printing boxes for unicode bindersGravatar Ralf Jung2018-06-10
|
* Merge PR #7690: Fixing typos in file Berardi.vGravatar Pierre-Marie Pédrot2018-06-05
|\
* | Deprecate implicit tactic solving.Gravatar Pierre-Marie Pédrot2018-06-04
| |
| * Fixing typos in file Berardi.vGravatar Hugo Herbelin2018-06-03
|/ | | | | Note that one of them is in the name of the main theorem, so we use a compatibility notation.
* Protecting against a "deprecated cofix" warning.Gravatar Hugo Herbelin2018-04-16
|
* [ltac] Deprecate nameless fix/cofix.Gravatar Emilio Jesus Gallego Arias2018-04-13
| | | | | | | | | | | | 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.
* Merge PR #6820: Tacticals assert_fails and assert_succeedsGravatar Maxime Dénès2018-03-09
|\
* \ Merge PR #6155: Get rid of ' notation for Zpos in QArithGravatar Maxime Dénès2018-03-09
|\ \
* \ \ Merge PR #6937: Add empty compat file for Coq 8.8Gravatar Maxime Dénès2018-03-09
|\ \ \
* \ \ \ Merge PR #6522: Fix core hint database issue #6521Gravatar Maxime Dénès2018-03-08
|\ \ \ \
* \ \ \ \ Merge PR #6743: Add notation {x & P} for sigTGravatar Maxime Dénès2018-03-08
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6909: Deprecate Focus and UnfocusGravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \
* | | | | | | [stdlib] Do not use “Require” inside sectionsGravatar Vincent Laporte2018-03-07
| | | | | | |
| | | | * | | Add empty compat file for Coq 8.8Gravatar Jason Gross2018-03-07
| |_|_|/ / / |/| | | | | | | | | | | | | | | | | This closes #6598
* | | | | | Merge PR #6744: Add String.concatGravatar Maxime Dénès2018-03-07
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\ \ \ \ \ \ \
| | | * | | | | Remove all uses of Focus in standard library.Gravatar Théo Zimmermann2018-03-04
| | | | | | | |
* | | | | | | | Remove 8.5 compatibility support.Gravatar Théo Zimmermann2018-03-02
| | | | | | | |
* | | | | | | | Remove VOld compatibility flag.Gravatar Théo Zimmermann2018-03-02
| | | | | | | |
* | | | | | | | Turn warning for deprecated notations on.Gravatar Théo Zimmermann2018-03-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Fix new deprecation warnings in the standard library.
* | | | | | | | Remove the deprecation for some 8.2-8.5 compatibility aliases.Gravatar Théo Zimmermann2018-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.Gravatar Hugo Herbelin2018-02-28
| | | | | | |
| | | | | | * Added tacticals assert_succeeds/assert_fails (courtesy of Jason Gross).Gravatar Hugo Herbelin2018-02-28
| | | | | | |
* | | | | | | Merge PR #6852: [stdlib] move “Require” out of sectionsGravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #1026: changed statements of Rpower_lt and Rle_power and added lemmasGravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \ \
| | | * | | | | | Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
| |_|/ / / / / / |/| | | | | | |
| | * | | | | | [stdlib] move “Require” out of sectionsGravatar Vincent Laporte2018-02-27
| |/ / / / / / |/| | | | | |
| | * | | | | Add String.concatGravatar Jason Gross2018-02-24
| |/ / / / / |/| | | | |
* | | | | | Merge PR #6599: Decimals in preludeGravatar Maxime Dénès2018-02-24
|\ \ \ \ \ \ | |_|_|_|_|/ |/| | | | |
* | | | | | Merge PR #6282: proposed fix for issue #3213: extra variable m in Lt.S_predGravatar Maxime Dénès2018-02-21
|\ \ \ \ \ \
| | * | | | | Decimal goodies : conversion to/from Coq stringsGravatar Pierre Letouzey2018-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 bijectionsGravatar Pierre Letouzey2018-02-20
| | | | | | |
| | * | | | | Decimal: simple representation of base-10 numbersGravatar Pierre Letouzey2018-02-20
| | | | | | |
* | | | | | | Trying a hack to support {'pat|P} without breaking compatibility.Gravatar Hugo Herbelin2018-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.Gravatar Hugo Herbelin2018-02-20
| | | | | | |
* | | | | | | More structured printing in unicode notations for binders.Gravatar Hugo Herbelin2018-02-20
| | | | | | |
* | | | | | | User-level support for Gonthier-Ssreflect's "if t then pat then u else v".Gravatar Hugo Herbelin2018-02-20
| |/ / / / / |/| | | | |
* | | | | | Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead.Gravatar Maxime Dénès2018-02-19
|\ \ \ \ \ \
| | | | * | | Add notation {x & P} for sigTGravatar Tej Chajed2018-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 transparentGravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \
* | | | | | | Document between and exists_between types.Gravatar Ismail2018-01-08
| | | | | | |
| | * | | | | Remove dir-locals and ship suggested helper hooks instead.Gravatar Gaëtan Gilbert2018-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 #6521Gravatar Anton Trunov2018-01-03
| |_|_|/ / |/| | | |
* | | | | Fix warning about shadowing a global name.Gravatar Gaëtan Gilbert2017-12-19
| | | | |
* | | | | Add named timers to LtacProfGravatar Jason Gross2017-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_factsGravatar Maxime Dénès2017-12-12
|\ \ \ \ \
* | | | | | Axiom-free proof of eta expansion.Gravatar Jasper Hugunin2017-12-11
| | | | | |