| Age | Commit message (Collapse) | Author |
|---|
|
Cf CHANGES for details.
|
|
|
|
|
|
Coq locations already had support for this, but were containing dummy
information. We now don't need anymore to reconstruct this information by
browsing the file when printing an error message or enriching exceptions on the
fly.
It also became easier to interface with Coq since locations emitted by the
lexer now always contain full information.
On the API side, Loc.represent disappeared and Loc.t is now exposed as record.
It is less error-prone than manipulating a tuple of 5 integers. Also,
Loc.create takes 5 arguments instead of 3 and a pair.
|
|
simplifying and generalizing the grammar entries for injection,
discriminate and simplify_eq.
|
|
In pat%constr, creating new evars is now allowed only if "eintros" is
given, i.e. "intros" checks that no evars are created, and similarly
e.g. for "injection ... as ... pat%constr".
The form "eintros [...]" or "eintros ->" with the case analysis or
rewrite creating evars is now also supported.
This is not a commitment to say that it is good to have an e- modifier
to tactics. It is just to be consistent with the existing convention.
It seems to me that the "no e-" variants are good for beginners. However,
expert might prefer to use the e-variants by default. Opinions from
teachers and users would be useful.
To be possibly done: do that [= ...] work on hypotheses with side
conditions or parameters based on the idea that they apply the full
injection and not only the restriction of it to goals which are
exactly an equality, as it is today.
|
|
It is already very old (shipped with Debian oldstable) and adds file name
support in locations.
|
|
Suggested by R. Krebbers and C. Cohen, this makes modes
more applicable, by allowing to trigger resolution on partially
instantiated indices. This is a rough but fast approximation of the
pattern on which one would like instances to apply.
|
|
|
|
simpler re-printing of assert.
Also fixing the precedence for printing "by" clause.
|
|
|
|
|
|
|
|
|
|
Note that this breaks the compatibility, in a beneficial way I believe. Tactics
defined in strict mode (i.e. through Ltac foo := ...) may not do an introduction
on a local identifier anymore. They must use the "fresh" primitive instead.
|
|
|
|
|
|
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.
|
|
This made little sense, as all the uses of this function were actually
called from toplevel ML modules. This was at best useless, and at worst
a source of bugs when loading plugins and messing with backtracking.
|
|
Instead of leaving the responsibility of extending the grammar to the caller,
we ask for a list of extensions in the return value of the function.
|
|
|
|
|
|
|
|
|
|
This was probably wreaking havoc in tricky undo-redo scenarii.
|
|
|
|
This removes the last call to unsafe_grammar_extend, so that all handwritten
grammar extensions are now type-safe. Grammars defined by CAMLPX EXTEND are
still using the unsafe interface, but as they insert explicit casts they are
deemed safe.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This reverts commit bde36d4b00185065628324d8ca71994f84eae244.
|
|
This reverts commit 857dc0aaae30805725da213b6550dc1ff3a7adb2.
|
|
|
|
allows for a simpler re-printing of assert.
Also fixing the precedence for printing "by" clause.
|
|
|
|
|
|
|
|
location set by lexer). This improves on abb4e7b0c by recovering the
lexer location.
AFAICS, it has an effect on lexer's errors Unterminated_comment and
Unterminated_string. The other errors were not wrongly located,
presumably because the Exc_located location added by camlp5 coincided
with the location given by the lexer.
|
|
into JasonGross-trunk-function_scope
|
|
It was only used by setoid_ring for the Add Ring command, and was easily
replaced by a dedicated argument. Moreover, it was of no use to tactic
notations.
|
|
|
|
We provide an API so that external code such as plugins can define grammar
extensions synchronized with the summary. This API is not perfect yet and is
a mere abstraction of the current behaviour. In particular, it expects the
user to modify the parser in an imperative way.
|
|
|
