| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
|
|
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.
|
|
|
|
automatically instead
|
|
|
|
|
|
|
|
As requested in
https://github.com/coq/coq/pull/384#issuecomment-303809461
|
|
As requested in
https://github.com/coq/coq/pull/384#issuecomment-303809461
|
|
Forwards/backwards reasoning thoughts come from
https://github.com/coq/coq/pull/385#discussion_r111008347
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
As per Hugo's request.
|
|
|
|
|
|
As per Hugo's suggestion in
https://github.com/coq/coq/pull/384#issuecomment-264891011
|
|
This tactic does better than [inversion] at sigma types.
|
|
|
|
As per Hugo's request.
|
|
As per Hugo's request in
https://github.com/coq/coq/pull/384#issuecomment-264891011
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
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].
|
|
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
|
|
|
|
|
|
|
|
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`).
|
|
|
|
|
|
|
|
|
|
No need to use `discriminate`. This is the hopefully uncontroversial part of https://github.com/coq/coq/pull/401.
|
|
discharge literal comparisons.
|
|
|
|
comparisons.
|
|
|
