| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
with evars).
|
|
|
|
|
|
|
|
|
|
|
|
dependencies
|
|
This development of @bmsherman tests universe polymorphism and setoid
rewriting in type, and should build with v8.6 and trunk.
|
|
- Fixing a typo introduced in 31dbba5f.
- Adapting to computation of universe constraints in pretyping.
- Adding a regression test.
|
|
|
|
|
|
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.
|
|
The fix follows an invariant enforced in proofview.ml on the kind of
evars that are goals or that occur in goals.
One day, evar kinds will need a little cleaning...
PS: This is a second attempt, completing db28e82 which was missing the
case PEvar in constr_matching.ml. Indeed the attached fix to #5487
alone made #2602 failing, revealing that the real cause for #2602 was
actually not fixed and that if the test for #2602 was working it was
because of #5487 hiding the real problem in #2602.
|
|
The cause was a missing evar/evar clause in ltac pattern-matching
function (constr_matching.ml).
|
|
|
|
|
|
reason I overlooked the result, maybe a missing make clean.
As for testing on the travis test architecture, I could have done
it. This is a question of compromise. I was so certain that it would
work that I did not test. And anyway, the travis test is not absolute
either.
In any case, I'm very sorry about the confusion it introduced.
~~~~ BY THE WAY, NO NEED TO SHOUT ~~~~
~~~~ IT IS A BIG MISCONCEPTION ABOUT HUMAN BEINGS ~~~~
~~~~ TO BELIEVE THAT THEY DO MISTAKES INTENTIONALLY ~~~~
Thank you!
|
|
|
|
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?).
|
|
|
|
One day I'll get bored of spending my nights fixing commits that were
pushed without being tested, and I'll ask for removal of push rights.
But for now let's pretend I haven't insisted enough:
~~~~ PLEASE TEST YOUR COMMITS BEFORE PUSHING ~~~~
Thank you!
|
|
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.
|
|
The fix follows an invariant enforced in proofview.ml on the kind of
evars that are goals or that occur in goals.
One day, evar kinds will need a little cleaning...
|
|
let-ins
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
