| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
| |
and global for 8.4 and 8.5.
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
An Ltac trace printing mechanism was introduced in 8.4 which was
inadvertedly modified by a series of commits such as 8e10368c3,
91f44f1da7a, ...
It was also sometimes buggy, iirc, when entering ML tactics which
themselves were calling ltac code.
It got really bad in 8.5 as in:
Tactic Notation "f" constr(x) := apply x. Ltac g x := f x.
Goal False.
idtac; f I. (* bad location reporting *)
g I. (* was referring to tactic name "Top.Top#<>#1" *)
which this commit fixes.
I don't have a clear idea of what would be the best ltac tracing
mechanism, but to avoid it to be broken without being noticed, I
started to add some tests.
Eventually, it might be worth that an Ltac expert brainstrom on it!
|
| | | |
|
| | | |
|
| | | |
|
| |\ \ |
|
| |/ / |
|
| |\ \ |
|
| | | | |
|
| | | | |
|
| |/ / |
|
| |\ \ |
|
| |\ \ \
| | | |
| | | |
| | | |
| | | | |
Note that this breaks a few badly written scripts using intro in strict
mode without providing an existing identifier.
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| |/ / / |
|
| |\ \ \ |
|
| | | | | |
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
#4770).
This also fixes comments not being properly skipped when looking for eol.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
As a side effect, there should be a small speedup when ignoring comments.
This commit also fixes two bugs related to handling "$$" and "#" in
comments.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This breaks compilation via ocamlbuild, and also leads to awkward
commands via make
|
| | |_|/ /
|/| | |
| | | |
| | | | |
Thanks to HH for pointing it out.
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This makes the core free from particular protocol choices.
It should help with the ppx serialization project and shrinks clib.cma a
bit.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This eases the task of replacing/improving the serializer, as well as
making it more resistant. See pitfalls below:
Main changes are:
- fold `message` type into `feedback` type
- make messages of type `Richpp.richpp` so we are explicit about the
content being a rich document.
- moved serialization functions for messages and stateid to `Xmlprotocol`
- improved a couple of internal API points (`is_message`).
Tested.
|
| |/ / / /
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Serialization should be specific to each particular backend, so we let
the Stm clients choose how the send the nodes.
This should be quite safe to pull in. Test suite passes.
Related to #180
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | | |
This brings a 10x speedup for going at the end of large .v files.
|
| |\ \ \ \ |
|
| | | | | | |
|
| |/ / / /
| | | |
| | | |
| | | | |
This brings a 10x speedup for going at the end of large .v files.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
functions about interpretation, internalization, externalization of
notations.
Main syntactic changes:
- subst_aconstr_in_glob_constr -> instantiate_notation_constr
(because aconstr has been renamed to notation_constr long time ago)
- extern_symbol -> extern_notation
(because symbol.ml has been renamed to notation.ml long time ago)
- documentation of notations_ops.mli
Main semantic changes:
- Notation_ops.eq_glob_constr which was partial eq disappears: use
glob_constr_eq instead
- In particular, this impacts a change on funind which now use the
(fully implemented) glob_constr_eq
Somehow, instantiate_notation_constr should be in notation_ops.ml for
symmetry with match_notation_constr but it is bit painful to do.
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | | |
For Drop for example.
|
| | | | |
| | | |
| | | |
| | | | |
and Evar in notations, and there are anyway already forbidden.
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | | |
uniformity.
|
| |\| | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
- the particlar rule for dev/printers.cma is adapted as for %.cma:%.mllib
- some more removal of | .d in rules
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We add a dependency of .cma over .mllib.
This dependency over the .mllib is somewhat artificial, since
ocamlc -a won't use this file, hence the $(filter-out ...) below.
But this ensures that the .cm(x)a is rebuilt when needed,
(especially when removing a module in the .mllib).
We also remove all "order-only" dependencies over *.d in rules,
since the -include mechanism should already ensure that we have
up-to-date dependencies known by make.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
There were a forgotten CAMLP4DEPS macro.
We also avoid otags failure with camlp5 (in this case, it only
builds the tags of regular .ml files, not .ml4).
|
| | | | | |
|
| | | | | |
|
| |\ \ \ \ |
|
Hugo Herbelin
Maxime Dénès
Enrico Tassi
Pierre-Marie Pédrot
Guillaume Melquiond
Pierre Letouzey
Emilio Jesus Gallego Arias
Lionel Rieg
Matthieu Sozeau