| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
This appends the currently selected word to the query. Only queries
that end with this are supported, "..." inside the query will just
not work.
|
|
|
|
|
|
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.
|
|
The command line option is named:
- async-proofs-delegation-threshold
Values are of type float, default 1.0 (seconds).
Proofs taking less that the threshold are not delegated to
a worker.
|
|
|
|
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.
|
|
Return the most appropriate evar_map for commands that can run on
non-focused proofs (like Check, Show and debug printers) so that
universes and existentials are printed correctly (they are global
to the proof). The API is backwards compatible.
|
|
|
|
Follow-up on Hugo's 1412f9f9.
|
|
- In Program, a check_evars_are_solved was introduced
too early. Program does it's checking of evars by itself.
- In Function, the universe environments were not threaded
correctly.
|
|
|
|
Use the compatibility match construction to extract the compatibility
constant associated to a primitive projection.
|
|
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).
|
|
|
|
Anomaly: Uncaught exception Unix.Unix_error(Unix.EACCES, "open", "lia.cache").
Please report.
|
