aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Collapse)AuthorAge
* Merge PR#375: DeprecationGravatar Maxime Dénès2017-06-15
|\
* \ Merge PR#753: Fix bug 5026 (the stdlib shouldn't define inconsistent notations).Gravatar Maxime Dénès2017-06-14
|\ \
* | | 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.
| | * Remove deprecated options from the standard library.Gravatar Guillaume Melquiond2017-06-14
| | |
| | * Remove support for Coq 8.4.Gravatar Guillaume Melquiond2017-06-14
| |/ |/|
* | Merge PR#498: Bignums as a separate opam packageGravatar Maxime Dénès2017-06-14
|\ \
* \ \ Merge PR#385: Equality of sigma typesGravatar Maxime Dénès2017-06-13
|\ \ \
| | * | BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Gravatar Pierre Letouzey2017-06-13
| |/ / |/| | | | | | | | | | | | | | See now https://github.com/coq/bignums Int31 is still in the stdlib. Some proofs there has be adapted to avoid the need for BigNumPrelude.
* | | Remove remaining vo.itarget files (obsolete since PR #499)Gravatar Pierre Letouzey2017-06-10
| | |
| | * 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
| |_|/ |/| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 23:54:02 +0000