aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init
Commit message (Collapse)AuthorAge
* Merge PR #6820: Tacticals assert_fails and assert_succeedsGravatar 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 #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\ \ \ \
* | | | | 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
| | | | |
| * | | | Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/ / / /
* | | | Merge PR #6599: Decimals in preludeGravatar Maxime Dénès2018-02-24
|\ \ \ \ | |_|_|/ |/| | |
| * | | 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
| | | |
* | | | User-level support for Gonthier-Ssreflect's "if t then pat then u else v".Gravatar Hugo Herbelin2018-02-20
|/ / /
| * / 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.
| * Fix core hint database issue #6521Gravatar Anton Trunov2018-01-03
|/
* 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.
* Moving bug numbers to BZ# format in the source code.Gravatar Théo Zimmermann2017-10-19
| | | | | Compared to the original proposition (01f848d in #960), this commit only changes files containing bug numbers that are also PR numbers.
* A little reorganization of notations + a fix to #5608.Gravatar Hugo Herbelin2017-08-29
| | | | | | | | | | | | | | - 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.
* Fix typo in documentation for identityGravatar Tej Chajed2017-07-05
| | | | Fixes Coq bug 5635 (https://coq.inria.fr/bugs/show_bug.cgi?id=5635).
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* plugins/ltac : avoid spurious .cmxs filesGravatar Pierre Letouzey2017-06-15
| | | | | | | | | | | | | | In the previous setting, all plugins/ltac/*.cmxs except ltac_plugin.cmxs (for instance coretactics.cmxs, g_auto.cmxs, ...) were utterly bogus : - wrong -for-pack used for their inner .cmx - dependency over modules not provided (for instance Tacenv, that ends up being a submodule of the pack ltac_plugin). But we were lucky, those files were actually never loaded, thanks to the several DECLARE PLUGIN inside coretactics and co, that end up in ltac_plugin, and hence tell Coq that these modules are already known, preventing any attempt to load them. Anyway, this commit cleans up this mess (thanks PMP for the help)
* Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
| | | | | | | | | | | | | | | | | The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted.
* Merge PR#385: Equality of sigma typesGravatar Maxime Dénès2017-06-13
|\
* | drop vo.itarget files and compute the corresponding the corresponding values ↵Gravatar Matej Kosik2017-06-01
| | | | | | | | automatically instead
| * More uniform indentation of sigma lemmasGravatar Jason Gross2017-05-28
| |
| * Give explicit proof terms to proj2_sig_eq etc.Gravatar Jason Gross2017-05-28
| |
| * Use the rew dependent notation in ex, ex2 proofsGravatar Jason Gross2017-05-28
| |
| * Make theorems about ex equality QedGravatar Jason Gross2017-05-28
| | | | | | | | | | As requested in https://github.com/coq/coq/pull/384#issuecomment-303809461
| * Make new proofs of equality QedGravatar Jason Gross2017-05-28
| | | | | | | | | | As requested in https://github.com/coq/coq/pull/384#issuecomment-303809461
| * Add some more comments about sigma equalitiesGravatar Jason Gross2017-05-28
| | | | | | | | | | Forwards/backwards reasoning thoughts come from https://github.com/coq/coq/pull/385#discussion_r111008347
| * Remove motive argument from [rew dependent]Gravatar Jason Gross2017-05-28
| |
| * Use a local [rew dependent] notationGravatar Jason Gross2017-05-28
| |
| * Add forward-chaining versions: [eq_sig*_uncurried]Gravatar Jason Gross2017-05-28
| |
| * Use notation for sigTGravatar Jason Gross2017-05-28
| |
| * Remove reference to [IsIso]Gravatar Jason Gross2017-05-28
| |
| * Use notations for [sig], [sigT], [sig2], [sigT2]Gravatar Jason Gross2017-05-28
| |
| * Use extended notation for ex, ex2 typesGravatar Jason Gross2017-05-28
| |
| * Replace [ex'] with [ex]Gravatar Jason Gross2017-05-28
| | | | | | | | | | | | | | | | | | The ' was originally denoting that we were taking in the projections and applying the constructor in the conclusion, rather than taking in the bundled versions and projecting them out (because the projections don't exist for [ex] and [ex2]). But we don't have versions like this for [sig] and [sigT] and [sigT2] and [sig2], so we might as well not add the ' to the [ex] and [ex2] versions.
| * Use [rew_] instead of [eq_rect_] prefixGravatar Jason Gross2017-05-28
| | | | | | | | As per Hugo's request.
| * Add equality lemmas for sig2 and sigT2Gravatar Jason Gross2017-05-28
| |
| * Add lemmas for ex2Gravatar Jason Gross2017-05-28
| |
| * Use [rew] notations rather than [eq_rect]Gravatar Jason Gross2017-05-28
| | | | | | | | | | As per Hugo's suggestion in https://github.com/coq/coq/pull/384#issuecomment-264891011
| * Add an [inversion_sigma] tacticGravatar Jason Gross2017-05-28
| | | | | | | | This tactic does better than [inversion] at sigma types.
| * Add lemmas about equality of sigma typesGravatar Jason Gross2017-05-28
| |
| * Use [rew_] instead of [eq_rect_] prefixGravatar Jason Gross2017-05-28
| | | | | | | | As per Hugo's request.
| * Use [rew] notations rather than [eq_rect]Gravatar Jason Gross2017-05-28
| | | | | | | | | | As per Hugo's request in https://github.com/coq/coq/pull/384#issuecomment-264891011
| * Add more groupoid-like theorems about [eq]Gravatar Jason Gross2017-05-28
|/
* Merge PR#201: Transparent abstractGravatar Maxime Dénès2017-05-11
|\
* \ Merge PR#605: Report a useful error for dependent inductionGravatar Maxime Dénès2017-05-05
|\ \