| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Suggests in some cases the right bullet to use.
|
|
|
|
If [i] or [j] is negative goals are counted from the end.
|
|
[cycle 1] puts the first goal last, [cycle -1] puts the last goal first, [cycle n] is like [do n cycle 1], [cycle -n] is like [do n cycle -1].
|
|
|
|
Fixes bug #3457
|
|
Thanks to E. Tassi for the initial patch.
|
|
|
|
|
|
The new implementation is made of two layers: a iolist, which is essentially
a stream without memoization, and above this a state monad. The previous
design of the extracted monad kept three distinct but similar monad
transformers: a stateT, a writerT and a readerT. We take advantage of this
similarity to pack those three transformers into only one state monad.
This makes the code cleaner and hopefully more efficient.
|
|
When starting proofs with [start_dependent_proof], we may have initial goals with existential variables in their conclusion. They will be solved by the proof, but this information was not propagated in close proof, and the kernel failed on uninstanciated evars.
|
|
|
|
telescope.
Allows for a more refined notion of dependently generated initial goals.
|
|
universe context to start proofs.
It was kind of awkward to work with for non-traditionnal kinds of proofs: if you have an evar_universe_context, you got it from a sigma anyway.
|
|
|
|
backtracks, print time spent in each of successive calls.
|
|
LoadedFile is generated when a .vo is loaded
Goals is generated when -feedback-goals
|
|
Experimenting with PIDE I discovered that yield is not sufficient
to have a rescheduling, hence the delay.
|
|
|
|
This reverts commit abad0a15ac44cb5b53b87382bb4d587d9800a0f6.
|
|
|
|
|
|
|
|
exhibits the "useless goal" behaviour: there is code out there depending on
the fact that goals cannot be solved by side effects.
|
|
|
|
|
|
|
|
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.
|
|
layer. To this intent, we add a cache evar_map in goals that is the
latest known one where the goal is nf-evarized. If the current one
and the cache coincide, we leave the goal as-is.
|
|
|
|
a projection constant only of the form
λ params (r : I params), match r with BuildR args => args_i end, without any
other user input and relies on it being typable (no more primitive projections
escaping this).
|
|
restriction, after last fix commit which precisely possibly restricts
evars of a term "t" in "apply t in H" without resolving them.
|
|
name of replaced hypothesis.
|
|
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.
|
|
|
|
different places
|
|
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
|
|
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.
|
|
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.
|
|
|
|
evar_map
in tactics, avoiding useless and potentially costly merge's of constraints.
- Implement revert and generalize using the new tactics (not bound to syntax though,
as they are not backwards-compatible yet).
|
|
in the Evd of proofs (Evd.from_env).
- Allow to set the Store.t value of new evars, e.g. to set constraint evars as
unresolvable in rewrite.ml.
- Fix a HUGE performance problem in the processing of constraints, which was remerging
all the previous constraints with the ambient global universes at each new constraint addition.
Performance is now back to (or better than) normal.
|
|
|
|
indeed unifies
with the projected term, keeping track of universes).
- Fix the [unify] tactic to fail properly.
- Fix unification to disallow lowering a global Type(i) universe to Prop or Set.
|
|
- Fix passing of universe contexts through definitions/proofs, abstract is ok now, even
in presence of polymorphism
- Correctly mark unresolvable the evars made by the Simple abstraction.
|
|
- Remove Universe Polymorphism flags everywhere.
- Properly infer, discharge template arities and fix substitution inside them
(kernel code to check for correctness).
- Fix tactics that were supposing universe polymorphic constants/inductives to
be parametric on that status. Required to make interp_constr* return the whole evar
universe context now.
- Fix the univ/level/instance hashconsing to respect the fact that marshalling doesn't preserve sharing,
sadly losing most of its benefits.
Short-term solution is to add hashes to these for faster comparison, longer term requires rewriting
all serialization code.
Conflicts:
kernel/univ.ml
tactics/tactics.ml
theories/Logic/EqdepFacts.v
|
