| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| | | | | | | |
|
| |\ \ \ \ \ \ |
|
| | |_|_|_|/ /
|/| | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This commits documents the as clause of specialize and that the
as clause of pose proof is optional.
It also mentions a feature of assert ( := ) that was available
since 8.5 and was mentionned by @herbelin in:
https://github.com/coq/coq/pull/248#issuecomment-297970503
|
| | | | | | | |
|
| | | | | | | |
|
| | |_|/ / /
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Off by default.
+ small refactoring of emacs hacks in printer.ml.
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ |
|
| | |_|_|_|_|_|_|/ /
|/| | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
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
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
Otherwise [(fun x => x) (Type : Type@{_})] becomes
[(fun x : Type@{i+1} => x) (Type@{i} : Type@{i+1})]
breaking the invariant that terms do not contain algebraic universes
(at the lambda abstraction).
|
| | | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
The addition to the test suite showcases the usage.
|
| |\ \ \ \ \ \ \ \ \
| |_|_|_|_|_|/ / /
|/| | | | | | | | |
|
| | |/ / / / / / /
|/| | | | | | | |
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | |/ / / / / /
|/| | | | | | |
|
| |\ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
dependencies
|
| | | | | | | | | | | | |
|
| | |_|_|_|_|_|_|_|_|/
|/| | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
Since 260965d, an imperative code was semantically the identity because the
closure allocation was not performed at the right moment. Because of it
intricacy, I cannot really tell the original motivations of this piece of
code, although it looks like it was for there for pretty-printing of errors.
Anyway, both because the code was dubious and its effect not observed, it
cannot hurt to remove it.
|
| | |/ / / / / / / /
|/| | | | | | | | |
|
| |/ / / / / / / / |
|
| | |_|_|_|_|_|/
|/| | | | | | |
|
| | |/ / / / /
|/| | | | |
| | | | | |
| | | | | | |
A universe substitution was lacking as the normalized evar map was dropped.
|
| | |_|_|_|/
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
The code was assuming that the terms t and u for which {t=u}+{t<>u} is
proved were distinct. We refine an internal "generalize" of "u" so
that it works on the two precise occurrences to abstract, even if
other occurrences of u occur as subterm of t too.
We also reuse the global constants found in the statement rather than
reconstructing them (this seems better in case the global constants
eventually get polymorphic universes?).
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | | |
This reverts commit 7bdfa1a4e46acf11d199a07bfca0bc59381874c3.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
I'm sure this was pushed by accident, since testing shows immediately
that it breaks the compilation of the ssreflect plugin, hence all
developments relying on it in Travis.
|
| | |_|_|/
|/| | | |
|
| | |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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`).
|
| | | |
| | |
| | |
| | | |
A priori considered to be a good programming style.
|
| | | |
| | |
| | |
| | |
| | | |
This highlights that this is a binary mode changing the interpretation
of "?x" rather than additionally allowing patvar.
|
| |\ \ \
| | | |
| | | |
| | | | |
let-ins
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
Maxime Dénès
Théo Zimmermann
Pierre Courtieu
Tej Chajed
Gaetan Gilbert
Abhishek Anand (@brixpro-home)
Pierre-Marie Pédrot
Hugo Herbelin
Guillaume Melquiond
Jason Gross