| Age | Commit message (Collapse) | Author |
|---|
|
Fix typo in proofview
|
|
with full backtracking across multiple goals.
|
|
simpler re-printing of assert.
Also fixing the precedence for printing "by" clause.
|
|
|
|
|
|
|
|
This allows to write things like this:
split; 2: intro _; exact I
or like this:
eexists ?[x]; ?[x]: exact 0; trivial
This has the side-effect on making the '?' before '[x]' mandatory.
|
|
|
|
Don't know however what should be the right guard to this try. Now
using catchable_exception, but even in 8.4, Failure was caught, which
is strange.
|
|
|
|
Now, type_scope is consistently used whether it is an hypothesis or
the conclusion, and consistently not used when in "context".
The question of a compatibility support, e.g., as suggested by Jason,
using a scope is still open though.
See reports #3050 and #4398.
|
|
The exact and e_exact tactics were not registering the universes and
constraints of the hint correctly. Now using the same connect_hint_clenv
as unify_resolve, they do. Also correct the implementation of
prepare_hint to normalize the universes of the hint before abstracting
its undefined universes. They are going to be refreshed at each
application. This means that eauto using term can
use multiple different instantiations of the universes of term
if term introduces new universes. If we want just one instantiation
then the term should be abbreviated in the goal first.
|
|
|
|
|
|
|
|
|
|
uniformity.
|
|
|
|
This reverts commit a66b57ba4bba866bb626bde2b6fe3b762347eb3e.
|
|
This patch splits pretty printing representation from IO operations.
- `Pp` is kept in charge of the abstract pretty printing representation.
- The `Feedback` module provides interface for doing printing IO.
The patch continues work initiated for 8.5 and has the following effects:
- The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`,
`pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`,
`msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be
used instead.
- Feedback provides different backends to handle output, currently,
`stdout`, `emacs` and CoqIDE backends are provided.
- Clients cannot specify flush policy anymore, thus `pp_flush` et al are
gone.
- `Feedback.feedback` takes an `edit_or_state_id` instead of the old
mix.
Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
|
|
Some dubious evarmap manipulation is going on in destruct because of the
use of clenv primitives. Here, building a clenv was introducing new evars
that were not taken into account in the remainder of the tactic. We plug
them back using a local workaround.
Eventually, this code should be replaced by an evar-based one, but meanwhile,
we rely on what is probably a hack.
|
|
|
|
Fix handling of non-polymorphic hints built from polymorphic values, or
simply producing new universes. We have to record the side effects of
global hints built from constrs which are not polymorphic when they
declare global universes, which might need to be discharged at the end
of sections too. Also issue a warning when a Hint is declared for a
polymorphic reference but the Hint isn't polymorphic itself (this used
to produce an anomaly). For [using] hints, treat all lemmas as
polymorphic, refreshing their universes at each use, as is done for
their existentials (also used to produce an anomaly).
|
|
|
|
|
|
It is indeed confusing, as it has little to do with the proper refine defined
in the New submodule. Legacy code relying on it should call the Logic or
Tacmach modules instead.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Although still working, it is now bad practice to use it, and it is not
widely spread anyway.
|
|
|
|
|
|
|
|
|
|
|
|
preserved, which is a source of incompatibilities w.r.t. released 8.5
but which looks to me to be the only possible canonical behavior.
This is I believe a better behavior than the Regular Subst Tactic
behavior in the released 8.5 and 8.5pl1. There, the order of
hypotheses in which substitutions happened was respected, but their
interleaving with other hypotheses was not respected.
So, I consider this to be a fix to the "Regular Subst Tactic" mode.
Also added a more detailed "specification" of the "Regular" behavior
of "subst" in the reference manual.
|
|
We only retype hypotheses and conclusion when they do depend on the cleared
identifier. This saves a lot of time.
|
|
This reverts commit bde36d4b00185065628324d8ca71994f84eae244.
|
