| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
| |
and avoiding explicit substitutions and merging of contexts, e.g. in obligations.ml.
The context produced by typechecking a statement is passed in the proof, allowing the
universe name context to be correctly folded as well. Mainly an API cleanup.
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
levels to A and B.
|
| |
|
|
|
|
| |
would change the
theory non-trivially.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
- Fix HoTT coq bug #80, implicit arguments with primitive projections were
wrongly automatically infered.
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
it was failing with Not_found before previous commit). This "fixes"
the loop by expanding local defs in "imitate" rather than keeping them
explicit. The example is otherwise too large for me to be able to
understand where does the loop come from.
|
| |
|
|
| |
- Remove dead code in evarconv.
|
| | |
|
| | |
|
| |
|
|
|
| |
bindings of the same variable (fixing HoTT bug #52). Document the unification
of universes in Ltac/tactics.
|
| |
|
|
| |
while Context gives different type to each variable, this test-suite file shows this.
|
| | |
|
| |
|
|
| |
- Move HoTT bug #30 to closed
|
| |
|
|
|
|
|
|
| |
of an anomaly in case
a universe inconsistency occurs when applying a coercion. The statement of the test-suite file
cannot check as is, but does check when the correct FunctorCategory is given, instantiating the TypeCat
to Set.
|
| |
|
|
|
|
| |
using explicit
universes. The behavior of Hint Rewrite still differs from Hint Resolve though.
|
| |
|
|
| |
name of replaced hypothesis.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
| |
I'd add more, but I'm tired and it's late and I should sleep. Maybe
I'll pick up at 3279 (working down) another day.
Bug 3344 is broken; [Fail Defined.] says that [Defined] has not failed,
even though it raises an anomaly. So there's no way I can think of to
test it. I've left it in the [opened] directory anyway.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
I've marked new failing commands that I'm confused about with "???"; I'm
not sure whether or not they should fail there, but we should keep the
test-suite compiling, probably.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
declare takes care of ignoring side effects that are available in the
global environment. This is yet another instance of what the "abominion"
(aka abstract) can do: the code was checking for the existence in the
environment of the elimination principle, and not regenerating it (nor
declaring the corresponding side effect) if the elimination principle
is used twice.
Of course to functionalize the imperative actions on the environment
when two proofs generated by abstract use the same elim principle,
such elim principle has to be inlined twice, once in each abstracted
proof. In other words, a side effect generated by a tactic inside
an abstract is *global* but will be made local, si it must always
be declared, no matter what.
Now the system works like this:
- side effects are always declared, even if a caching mechanism thinks
the constant is already there (it can be there, no need to regenerate it
but the intent to generate it *must* be declared anyhow)
- at Qed time, we filter the list of side effects and decide which ones are
really needed to be inlined.
bottom line: STOP using abstract.
|
| |
|
|
|
|
|
| |
foo@{(ident|Prop|Set|Type|' ')*}
(user given names are still write only).
- Add test-suite file for named universes.
|
| |
|
|
| |
- Finish the change to level-to-level substitutions, in the checker.
|
| |
|
|
|
|
|
| |
- Add a tentative syntax for specifying universes: Type{"i"} and foo@{Type{"i"},Type{"j"}}.
These are always rigid.
- Use level-to-level substitutions where the more general level-to-universe substitutions
were previously used.
|
| |
|
|
|
| |
Of course, this is an under approximation of the expected behavior : unfolding
a constant iff a leaf of its underlying split-tree is reached.
|
| | |
|
| |
|
|
| |
... as ..." which was not working. - Now applying the simplification on any "existT" generated by "injection" (possible source of incompatibilities).
|
| |
|
|
| |
not introduce beyond what is under control of the branch. See test-suite intros.v for an example.
|
| | |
|
| |
|
|
|
|
|
|
|
| |
correctly when comparing stacks.
- Disallow Type i <= Prop/Set constraints, that would otherwise allow
constraints that make a universe lower than Prop.
- Fix stm/lemmas that was pushing constraints to the global context,
it is done depending on the constant/variable polymorphic status now.
- Adapt generalized rewriting in Type code to these fixes.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
| |
The contract is that a file in bugs/opened should not raise errors if
the bug is still open.
Some of them fail for different reasons than they used to; I'm not sure
what to do about these.
|
Matthieu Sozeau
Hugo Herbelin
Jason Gross
Enrico Tassi
Pierre Boutillier
Pierre-Marie Pédrot