| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
Don't know if compare_cont is very useful to use, but, at least, these
extensions make sense.
|
|
This completes the series and cannot hurt.
|
|
|
|
This is needed to fix `Declare ML Module "ltac_plugin".
|
|
|
|
|
|
|
|
|
|
Tactic Notation
|
|
This performance bug was introduced 9 years ago in a8b0345, where the
responsibility of normalizing the term went from ccnv to eqappr in Reduction.
As a result, all recursive calls to eqappr that were preemptively reducing the
term ended up calling whd_stack twice, once by themselves, and once in the
subsequent call to eqappr.
This caused an important slowdown for conversion-intensive proofs, as the
whd_stack calls CClosure.zip to perfom in-place term sharing, leading to
useless huge re-allocations and repetitive write barriers.
Now that eqappr always head-normalizes the term beforehand, we simply don't
call whd_stack anymore when jumping to eqappr.
|
|
|
|
The syntax is: TACTIC EXTEND foo AT LEVEL i
This commit makes it possible to define tacticals like the ssreflect
arrow without having to resort to GEXTEND statements and intepretation
hacks.
Note that it simply makes accessible through the ML interface what Tactic
Notation already supports:
Tactic Notation (at level 1) tactic1(t) "=>" ipats(l) := ...
|
|
This reverts commit e8137ae63b3b19436755f372b595e7343e942894,
was meant for 8.6 branch only.
|
|
Hurkens.v by dropping the artificial need for monad laws. Tactic eauto
decided to be dependent on the laws but there is a shorter proof
without them.
[Interestingly, eauto is not able to find the short proof. This is a
situation of the form
subgoal 1: H : ?A |- P x
subgoal 2: H : M ?A |- M (forall x, P x)
where addressing the second subgoal would find the right instance of
?A, but this instance is too hard to find by addressing first the
first subgoal.]
|
|
|
|
|
|
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.
|
|
|
