| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
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).
|
|
|
|
|
|
|
|
We're back to a unique build phase (as before e372b72), but without
relying on the awkward include-deps-failed-lets-retry feature of make.
Since PMP has made grammar/ self-contained, we could now build
grammar.cma in a rather straightforward way, no need for
a specific sub-call to $(MAKE) for that. The dependencies between
files of grammar/ are stated explicitely, since .d files aren't
fully available initially.
Some Makefile simplifications, for instance remove the CAMLP4DEPS
shell horror. Instead, we generalize the use of two different
filename extensions :
- a .mlp do not need grammar.cma (they are in grammar/ and tools/compat5*.mlp)
- a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo),
except coqide_main.ml4 and its specific rule
Note that we do not generate .ml4.d anymore (thanks to the .mlp vs.
.ml4 dichotomy)
|
|
Coqdep_boot has almost no dependencies, and hence can be compiled
very early during the build, without relying on .ml.d files.
Some code of system.ml is now in a separate file minisys.ml,
which is also included in system.ml for compatibility.
|
|
If the second allocation causes a collection of the minor heap, the first
allocation will be freed, thus causing a memory corruption.
Note: it only happens when computing the native projection of an opaque
value while the minor heap is almost full.
|
|
|
|
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.
|
|
|
|
In particular, no more warning about ocamldep finding stuff both
in checker/ and kernel/.
A 'make clean' is mandatory after this commit
|
|
|
|
|
|
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.
|
|
Command line options to be dropped got outdated after vi -> vio renaming.
This made the par: goal selector do not work in conjunction with -quick.
|
