aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init
Commit message (Collapse)AuthorAge
* 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
|\ \
* \ \ Merge PR#593: Functional choice <-> [inhabited] and [forall] commuteGravatar Maxime Dénès2017-05-05
|\ \ \
| | * | 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].
| * | | Functional choice <-> [inhabited] and [forall] commuteGravatar Gaetan Gilbert2017-04-30
| |/ /
* / / 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#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 branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-15
|\
* \ 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.
* | | \ Merge PR#442: Allow interactive editing of Coq.Init.LogicGravatar Maxime Dénès2017-03-17
|\ \ \ \
* \ \ \ \ Merge PR#451: Add η principles for sigma typesGravatar Maxime Dénès2017-03-17
|\ \ \ \ \
| | | * | | Farewell decl_modeGravatar Enrico Tassi2017-03-07
| |_|/ / / |/| | | | | | | | | | | | | | | | | | | This commit removes from the source tree plugins/decl_mode, its chapter in the reference manual and related tests.
* | | | | A couple of other useful properties about compare_cont.Gravatar Hugo Herbelin2017-03-03
| | | | | | | | | | | | | | | | | | | | | | | | | Don't know if compare_cont is very useful to use, but, at least, these extensions make sense.
* | | | | Compatibility of iff wrt not and imp.Gravatar Hugo Herbelin2017-03-03
| | | | | | | | | | | | | | | | | | | | This completes the series and cannot hurt.
| * | | | Add η principles for sigma typesGravatar Jason Gross2017-03-01
| | | | |
| * | | | Remove some trailing whitespace in Init/Specif.vGravatar Jason Gross2017-03-01
|/ / / /
| | | * Fixing a little bug in printing ex2 (type was printed "_" by default).Gravatar Hugo Herbelin2017-02-23
| | | |
| * | | Allow interactive editing of Coq.Init.LogicGravatar Jason Gross2017-02-21
|/ / / | | | | | | | | | | | | Without this change, coqtop complains that I need to require Coq.Init.Logic to use [replace ... with ... by ...].
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 17:59:20 +0000