aboutsummaryrefslogtreecommitdiff
path: root/theories/Init
AgeCommit message (Collapse)Author
2017-06-13Merge PR#385: Equality of sigma typesMaxime Dénès
2017-06-01drop vo.itarget files and compute the corresponding the corresponding values ↵Matej Kosik
automatically instead
2017-05-28More uniform indentation of sigma lemmasJason Gross
2017-05-28Give explicit proof terms to proj2_sig_eq etc.Jason Gross
2017-05-28Use the rew dependent notation in ex, ex2 proofsJason Gross
2017-05-28Make theorems about ex equality QedJason Gross
As requested in https://github.com/coq/coq/pull/384#issuecomment-303809461
2017-05-28Make new proofs of equality QedJason Gross
As requested in https://github.com/coq/coq/pull/384#issuecomment-303809461
2017-05-28Add some more comments about sigma equalitiesJason Gross
Forwards/backwards reasoning thoughts come from https://github.com/coq/coq/pull/385#discussion_r111008347
2017-05-28Remove motive argument from [rew dependent]Jason Gross
2017-05-28Use a local [rew dependent] notationJason Gross
2017-05-28Add forward-chaining versions: [eq_sig*_uncurried]Jason Gross
2017-05-28Use notation for sigTJason Gross
2017-05-28Remove reference to [IsIso]Jason Gross
2017-05-28Use notations for [sig], [sigT], [sig2], [sigT2]Jason Gross
2017-05-28Use extended notation for ex, ex2 typesJason Gross
2017-05-28Replace [ex'] with [ex]Jason Gross
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.
2017-05-28Use [rew_] instead of [eq_rect_] prefixJason Gross
As per Hugo's request.
2017-05-28Add equality lemmas for sig2 and sigT2Jason Gross
2017-05-28Add lemmas for ex2Jason Gross
2017-05-28Use [rew] notations rather than [eq_rect]Jason Gross
As per Hugo's suggestion in https://github.com/coq/coq/pull/384#issuecomment-264891011
2017-05-28Add an [inversion_sigma] tacticJason Gross
This tactic does better than [inversion] at sigma types.
2017-05-28Add lemmas about equality of sigma typesJason Gross
2017-05-28Use [rew_] instead of [eq_rect_] prefixJason Gross
As per Hugo's request.
2017-05-28Use [rew] notations rather than [eq_rect]Jason Gross
As per Hugo's request in https://github.com/coq/coq/pull/384#issuecomment-264891011
2017-05-28Add more groupoid-like theorems about [eq]Jason Gross
2017-05-11Merge PR#201: Transparent abstractMaxime Dénès
2017-05-05Merge PR#605: Report a useful error for dependent inductionMaxime Dénès
2017-05-05Merge PR#593: Functional choice <-> [inhabited] and [forall] commuteMaxime Dénès
2017-05-03Report a useful error for dependent inductionTej Chajed
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].
2017-04-30Functional choice <-> [inhabited] and [forall] commuteGaetan Gilbert
2017-04-28Add .dir-locals.el and _CoqProject files for emacs stdlib editingJason Gross
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`).
2017-04-27Merge PR#584: Give andb_prop a simpler proofMaxime Dénès
2017-04-26Small typo in commentVadim Zaliva
2017-04-25Add transparent_abstract tacticJason Gross
2017-04-25Give andb_prop a simpler proofJason Gross
No need to use `discriminate`. This is the hopefully uncontroversial part of https://github.com/coq/coq/pull/401.
2017-04-15Merge branch 'v8.6' into trunkMaxime Dénès
2017-04-06Merge PR#455: Farewell decl_modeMaxime Dénès
2017-04-06Merge branch 'origin/v8.5' into v8.6.Hugo Herbelin
Was needed to be done for a while.
2017-03-17Merge PR#442: Allow interactive editing of Coq.Init.LogicMaxime Dénès
2017-03-17Merge PR#451: Add η principles for sigma typesMaxime Dénès
2017-03-07Farewell decl_modeEnrico Tassi
This commit removes from the source tree plugins/decl_mode, its chapter in the reference manual and related tests.
2017-03-03A couple of other useful properties about compare_cont.Hugo Herbelin
Don't know if compare_cont is very useful to use, but, at least, these extensions make sense.
2017-03-03Compatibility of iff wrt not and imp.Hugo Herbelin
This completes the series and cannot hurt.
2017-03-01Add η principles for sigma typesJason Gross
2017-03-01Remove some trailing whitespace in Init/Specif.vJason Gross
2017-02-23Fixing a little bug in printing ex2 (type was printed "_" by default).Hugo Herbelin
2017-02-21Allow interactive editing of Coq.Init.LogicJason Gross
Without this change, coqtop complains that I need to require Coq.Init.Logic to use [replace ... with ... by ...].
2017-02-17Ltac as a plugin.Pierre-Marie Pédrot
This commit is essentially moving files around. In particular, the corresponding plugin still relies on a mllib file rather than a mlpack one. Otherwise, this causes link-time issues for third-party plugins depending on modules defined in the Ltac plugin.
2016-10-24Remove v62 from stdlib.Théo Zimmermann
This old compatibility hint database can be safely removed now that coq-contribs do not depend on it anymore.
2016-07-18Replacing deprecated Implicit Arguments in prelude.Maxime Dénès
Was triggering a deprecation warning.
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-25 10:35:22 +0000