aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Collapse)AuthorAge
...
| | * Fix bug 5026 (the stdlib shouldn't define inconsistent notations).Gravatar Théo Zimmermann2017-06-08
| |/ |/|
* | 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
|/
* Stop using auto with * in two proofs.Gravatar Théo Zimmermann2017-05-16
| | | | | | auto with * is an overkill for people who do not care to understand what they really need. In these two cases, one lemma which was available in the typeclass_instances hint db.
* 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
|\ \
* \ \ Merge PR#593: Functional choice <-> [inhabited] and [forall] commuteGravatar Maxime Dénès2017-05-05
|\ \ \
* \ \ \ Merge PR#588: Allow interactive editing of {C,}Morphisms in PGGravatar Maxime Dénès2017-05-03
|\ \ \ \
* \ \ \ \ Merge PR#386: Better editing of the standard library in coqtop/PGGravatar Maxime Dénès2017-05-03
|\ \ \ \ \
| | | | * | Report a useful error for dependent inductionGravatar Tej Chajed2017-05-03
| |_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The dependent induction tactic notation is in the standard library but not loaded by default, leading to a parser error message that is confusing and unhelpful. This commit adds a notation for dependent induction to Init that fails and reports [Require Import Coq.Program.Equality.] is required to use [dependent induction].
| | | * | Reorganize comment documentation of ChoiceFacts.vGravatar Gaetan Gilbert2017-05-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Shortnames and natural language descriptions of principles are moved next to each principle. The table of contents is moved to after the principle definitions. Extra definitions are moved to the definition section (eg DependentFunctionalChoice) Compatibility notations have been moved to the end of the file. Details: The following used to be announced but were neither defined or used, and have been removed: - OAC! - Ext_pred = extensionality of predicates - Ext_fun_prop_repr = choice of a representative among extensional functions to Prop GuardedFunctionalRelReification was announced with shortname GAC! but shortname GFR_fun was used next to it. Only the former has been retained. Shortnames and descriptions have been invented for InhabitedForallCommute DependentFunctionalRelReification ExtensionalPropositionRepresentative ExtensionalFunctionRepresentative Some modification of headlines
| | | * | Functional choice <-> [inhabited] and [forall] commuteGravatar Gaetan Gilbert2017-04-30
| |_|/ / |/| | |
* | | | Suppress warning message in stdlib.Gravatar Guillaume Melquiond2017-04-29
| | | |
| | * | Allow interactive editing of {C,}Morphisms in PGGravatar Jason Gross2017-04-28
| |/ / |/| |
| * | Add .dir-locals.el and _CoqProject files for emacs stdlib editingGravatar Jason Gross2017-04-28
|/ / | | | | | | | | | | | | | | | | | | | | | | These set up PG to use the local coqtop, and the local coqlib, when editing files in the stdlib. As per https://github.com/coq/coq/pull/386#issuecomment-279012238, we can use `_CoqProject` for `theories/Init`, and this allows CoqIDE to edit those files. However, we cannot use it for `theories/`, because a `_CoqProject` file will override a `.dir-locals.el` in the same directory, and there is no way to get PG to pick up a valid `-coqlib` from `_CoqProject` (because it'll take the path relative to the current directory, not relative to the directory of `_CoqProject`).
* | Merge PR#414: Some more theory on powerRZ.Gravatar Maxime Dénès2017-04-27
|\ \
* \ \ Merge PR#584: Give andb_prop a simpler proofGravatar Maxime Dénès2017-04-27
|\ \ \
* | | | Small typo in commentGravatar Vadim Zaliva2017-04-26
| | | |
| | | * Add transparent_abstract tacticGravatar Jason Gross2017-04-25
| |_|/ |/| |
| * | Give andb_prop a simpler proofGravatar Jason Gross2017-04-25
|/ / | | | | No need to use `discriminate`. This is the hopefully uncontroversial part of https://github.com/coq/coq/pull/401.
* | Merge PR#545: Add some hints to the "real" database to automatically ↵Gravatar Maxime Dénès2017-04-19
|\ \ | | | | | | | | | discharge literal comparisons.
* \ \ Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-15
|\ \ \
| | * | Add some hints to the "real" database to automatically discharge literal ↵Gravatar Guillaume Melquiond2017-04-07
| |/ / |/| | | | | | | | comparisons.
* | | Merge PR#455: Farewell decl_modeGravatar Maxime Dénès2017-04-06
|\ \ \
| | * \ Merge branch 'origin/v8.5' into v8.6.Gravatar Hugo Herbelin2017-04-06
| | |\ \ | | | | | | | | | | | | | | | Was needed to be done for a while.
* | | | | Fix documentation typo (bug #5433).Gravatar Guillaume Melquiond2017-04-02
| | | | |
* | | | | Simplify some proofs.Gravatar Guillaume Melquiond2017-04-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit does not modify the signature of the involved modules, only the opaque proof terms. One has to wonder how proofs can bitrot so much that several occurrences of "replace 4 with 4" start appearing.
* | | | | Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R.Gravatar Guillaume Melquiond2017-03-30
| | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-04 01:21:39 +0000