| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
This was not working when the inductive type had implicit parameters.
This could still be improved. E.g. the following still does not work:
Reserved Notation "#".
Inductive I {A:Type} := C : # where "#" := I.
But it should be made working by taking care of adding the mandatory
implicit argument A at the time # is interpreted as [@I _]
(i.e., technically speaking, using expl_impls in interp_notation).
|
|
|
|
|
|
|
|
Without this change, coqtop complains that I need to require
Coq.Init.Logic to use [replace ... with ... by ...].
|
|
This is required since we merged PR#309: Ltac as a plugin.
|
|
|
|
This is in preparation for landing of PR#309: Ltac as a plugin
|
|
|
|
|
|
|
|
[ocamlbuild] fix small mistakes in descriptions
|
|
|
|
|
|
|
|
We unroll the map operation by hand in two performance-critical cases so as
not to call the generic array allocation function in OCaml, and allocate
directly on the minor heap instead. The generic array function is slow because
it needs to discriminate between float and non-float arrays. The unrolling
replaces this by a simple increment to the minor heap pointer and moves from
the stack.
The quantity of unrolling was determined by experimental measures on various Coq
developments. It looks like most of the maps are for small arrays of size lesser
or equal to 4, so this is what is implemented here. We could probably extend it
to an even bigger number, but that would result in ugly code. From what I've seen,
virtually all maps are of size less than 16, so that we could probably be almost
optimal by going up to 16 unrollings, but the code tradeoffs are not obvious. Maybe
when we have PPX?
|
|
|
|
|
|
|
|
|
|
This is cumbersome, because now code may fail at link time if it's not
referring to the correct module name. Therefore, one has to add corresponding
open statements a the top of every file depending on a Ltac module. This
includes seemingly unrelated files that use EXTEND statements.
|
|
This commit is essentially moving files around. In particular, the corresponding
plugin still relies on a mllib file rather than a mlpack one. Otherwise, this
causes link-time issues for third-party plugins depending on modules defined
in the Ltac plugin.
|
|
|
|
|
|
|
|
|
|
|
|
[travis] Add math-comp overlays, update CompCert to official version, add UniMath
|
|
|
|
We make math-comp overlays easier, we also start structuring the
scripts a bit more.
|
|
|
|
|
|
|
|
We extend `Stm.vernac_interp` so it can handle the commands it should
by level. This reenables `Show Script` handling, and this
interpretation function should handle more commands in the future such
as Load.
However note that we must first refactor the parsing state handling a
bit and remove the legacy `Stm.interp` before that.
|
|
Currently, the STM, vernac interpretation, and the toplevel are
intertwined in a mutual dependency that needs to be resolved using
imperative callbacks.
This is problematic for a few reasons, in particular it makes the
interpretation of commands that affect the document quite intricate.
As a first step, we split the `toplevel/` directory into two: "pure"
vernac interpretation is moved to the `vernac/` directory, on which
the STM relies.
Test suite passes, and only one command seems to be disabled with this
approach, "Show Script" which is to my understanding
obsolete. Subsequent commits will fix this and refine some of the
invariants that are not needed anymore.
|
|
For this, I used a new inductive type Z_spec to reason on Z.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Interpretation of patterns in Ltac is essentially flawed. It does a roundtrip
through the pretyper, and relies on suspicious flagging of evars in the evar source
field to recognize original pattern holes. After the pattern_of_constr function
was made evar-insensitive, it expanded evars that were solved by magical side-effects
of the pretyper, even if it hadn't been asked to perform any heuristics.
We backtrack on the insensitivity of the pattern_of_constr function. This may have
a performance penalty in other dubious code, e.g. hints. In the long run we should
get rid of the pattern_of_constr function.
|
|
|
|
The underlying hint mode implementation was not using the evar-insensitive
API so that it resulted in strange bugs.
|
|
Now they are useless because all of the primitives are (should?) be
evar-insensitive.
|
