| Age | Commit message (Collapse) | Author |
|---|
|
- More cleanup. remove unneeded functions in universes
|
|
|
|
handling from
the instance/contexts and substitution code.
|
|
|
|
Universes.
Needed to exponse compare_head_gen(_leq) so that it could be reused in Universes.
Remove unused functions from univ as well and refactor a little bit.
Changed the syntax to Type@{} for explicit universe level specs, following the WG decision.
|
|
|
|
into trunk
|
|
|
|
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.
|
|
reduction.
|
|
the checker, and it was not used before that anyway.
|
|
|
|
|
|
This should finally get rid of the following class of bugs:
Qed fails, STM undoes to the beginning of the proof because the
exception is not annotated with the correct state, PG gets out of
sync because errors always refer to the last command in PGIP.
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
as "forall x:nat*nat, x=x", which resulted in
"forall n n0 : nat, (n, n0) = (n, n0)" before commit
37f68259ab0a33c3b5b41de70b08422d9bcd3bec on "Fixing introduction
patterns * and ** ".
|
|
|
|
|
|
It grouped a list of vernac commands as a single one. It was undocumented and unused (and apparently unusable, because the intermediate '.' seem to be parsed as end of phrases by the interfaces). The main application could be to group the commands for Time. There is room for such an application in the syntax, but I unplugged the syntax for the time being.
The syntax would conflict with the use of a standalone dispatching tactical [ t1 | t2 | … | tn ].
I took the opportunity to separate the code dedicated to lists of commands in a separate type from vernac_expr.
|
|
allowing fast conversion to be used during unification while respecting the
semantics of unification w.r.t universes.
- Inside kernel, checked_conv is used mainly, it just does checking, while infer_conv
is used for module subtyping.
- Outside, infer_conv is wrapped in Reductionops to register the right constraints
in an evarmap.
- In univ, add a flag to universes to cache the fact that they are >= Set, the
most common constraints, resulting in an 4x speedup in some cases (e.g. HigmanS).
|
|
|
|
slightly more efficient than plain balanced maps.
|
|
|
|
induction/elim over a dependent elimination principle for Prop
arguments.
|
|
induction/elim over a dependent elimination principle for Prop
arguments.
|
|
different places
|
|
|
|
|
|
foo@{(ident|Prop|Set|Type|' ')*}
(user given names are still write only).
- Add test-suite file for named universes.
|
|
|
|
polymorphic
constants.
|
|
- 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.
|
|
to not interfere with already declared universes.
|
|
collapsed universes.
- Fix normalization with universe substitutions during refinement being inconsistent
with the one in the kernel.
|
|
Of course, this is an under approximation of the expected behavior : unfolding
a constant iff a leaf of its underlying split-tree is reached.
|
|
|
|
the GTac module. A ['a Gtac.t] is a special case of tactic that
may depend on the current goals, or not. Internally, it construct
a list of results, one for each focussed goal, if the tactic is
actually dependent.
This allows for an interpretation of whole-goal tactic that does
work, which was not the case for the previous implementation,
which did to many Proofview.Goal.enter.
|
|
|
|
|
|
|
|
destruction of schemes in Type such as sumbool.
Added an option "Set Standard Proposition Elimination Names" for
governing this strategy (activated by default).
This provides names supposingly more uniform than before for those who
like to have names automatically generated, at least in the first
phase of the development process of proofs.
Examples:
*** Non dependent case ***
Goal {True}+{False}-> True.
intros [|].
Before:
t : True
============================
True
and
f : False
============================
True
After:
H : True
============================
True
H : False
============================
True
*** Dependent case ***
Goal forall x:{True}+{False}, x=x.
intros [|].
Before:
t : True
============================
left t = left t
f : False
============================
right f = right f
After:
HTrue : True
============================
left HTrue = left HTrue
HFalse : False
============================
right HFalse = right HFalse
|
|
in Prop of constructors of inductive types independent of these names.
Incidentally upgraded/simplified a couple of proofs, mainly in Reals.
This prepares to the next commit about using names based on H for such
hypotheses in Prop.
|
|
... 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.
|
