| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
cases of Type (* Prop *) <= Set.
- Do check types of metavariables at the end of apply's unification,
if it failed at the beginning (otherwise universe constraints can be incomplete).
|
|
|
|
(refolding of cbn is smarter)
|
|
|
|
|
|
|
|
|
|
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.
|
|
needed during
unification.
|
|
- logical paths given to -R and -I should be split
on periods.
- it also seems like giving an empty string should
result in the empty path rather than the singleton
path with an empty string as an identifier.
|
|
conflicting with the previous behaviour of 'eexists'.
|
|
required"
I tested the commit on the wrong branch...
This reverts commit b0364eff4ec8ad5676060d8ca9cdbbb1d9c34d04.
|
|
writing a new primitive recovering the first goal under focus. It sounds a bit
hackish, but it does actually work.
|
|
proof. Indeed, computing an empty list of arguments triggered a
Proofview.Goal.enter, which broke tactics like [shelve_unifiable].
This does not fix this particular tactic though, because the Ltac
interpreter still enters the goal when calling a Ltac reference.
|
|
removing the strange kind of syntax "exists ,t,". which was equivalent to
"split; exists t; split", as in e.g.:
Goal (exists x, x=0) /\ (exists x, x=0).
exists ,0,.
Qed.
This answers bug request #3340.
|
|
variant of it, accepting an additional integer.
|
|
The call to the native compiler can fail due to the sheer amounts of -I
options passed to it. Indeed, it is easy to get the command line to exceed
512KB, thus causing various operating systems to reject it. This commit
avoids the issue by only passing the -I options that matter for the
currently compiled code.
Note that, in the worst case, this commit is still not sufficient on
Windows (32KB max), but this worst case should be rather uncommon and thus
can be ignored for now.
For the record, the command-line size mandated by Posix is 4KB.
|
|
|
|
|
|
|
|
parsing rule.
|
|
|
|
|
