| Age | Commit message (Collapse) | Author |
|---|
|
In compiler mode, only vernac.ml knows the current file name.
Stm.process_error_hook moved from Vernacentries to Vernac to
be bale to properly enrich the exception with the current file
name (if any).
|
|
|
|
|
|
We beta-iota normalize the type of the rewriting predicate to ensure that the
non-dependency in the arrow argument is meaningful. Otherwise, terms of the
form "forall x : A, (fun _ : A => P) x" generated by the retyping would confuse
the non-dependency heuristic.
|
|
|
|
|
|
|
|
preserving compatibility of subst after #4214 being solved.
|
|
(see #3695).
|
|
TACTIC EXTEND (based on user-given name).
|
|
|
|
Improving treatment of recursive equations compared to 8.4 (see test-suite).
Experimenting not to unfold local defs ever in subst.
(+ Slight simplification in checking reflexive equalities only once).
|
|
allow reusability of the implementation throughout the Coq codebase.
We effectively feature a generalized version of the logical monad where the
input state, the output state and the inner exception can be arbitrarily chosen.
This will allow for more efficient implementations of close variants of the
monad.
|
|
after patch for #4214 on subst needed to be repeated (see
857e82b2ca0d1).
|
|
|
|
|
|
|
|
The hypinfo cache was actually always set to None, so that there was no need
to try to preserve it if it was set to an actual value.
|
|
|
|
|
|
|
|
|
|
The command [Redirect "filename" (...)] redirects all the output of
[(...)] to file "filename.out". This is useful for storing the results of
an [Eval compute], for redirecting the results of a large search, for
automatically generating traces of interesting developments, and so on.
|
|
|
|
equalities in configurations like
x=y
x=z
===
P(x,y,z)
where it now produces
===
P(z,z,z)
In particular (equations are processed from most ancient to most recent).
Thanks to this, a "repeat subst" can just be a "subst" in List.v.
Incidentally: moved a nf_enter to enter in subst_one, since the latter
is normally called from other tactics having normalized evars.
|
|
- add a nra tactic (similar to nia) for non-linear real arithmetic tactic
- fix a long-standing bug in the reification code
- port to the new proof-engine
|
|
- Arithmetic operators and brackets are no longer recognized as bullets,
unless they follow a stop or start a line.
- Most vernacular commands are no longer highlighted when used inside
proof scripts.
- Coqdoc comments now take precedence over regular comments.
|
|
Option -g has no impact on the code generated by GCC, so it is now
systematically added, since it is quite helpful when the VM segfaults
(e.g. bug #4203). Note that, even for a debug build, option -O1 is
preferred to -O0, since -O0 produces assembly code that is much too noisy
for debugging.
For non-debugging builds, -O2 was chosen rather than -O3, since it led to
a noticeably faster VM. I guess even recent GCC compilers still have a
hard time optimizing humongous functions such as the VM.
Here are the results on a simple benchmark: computing the factorial of a
large number with Z and BigZ. (Factorial of 2*6! for Z, of 7! for BigZ.)
For comparison purpose, the timings of native_compute are also provided.
Z BigZ
-O0 6.4 12.3
-O1 4.3 10.7
-O2 2.8 7.3
-O3 3.0 9.3
n_c 2.0 2.4
|
|
|
|
|
|
|
|
Since error messages are ultimately passed to Format, which has its own
buffers for concatenating strings, using concatenation for preparing error
messages just doubles the workload and increases memory pressure.
|
|
|
|
|
|
Followup of: f7b29094fe7cc13ea475447bd30d9a8b942f0fef . In particular, re-closes #3593.
As a side effect, fixes an undiscovered bug of the `eq_constr` tactic which didn't consider terms up to evar instantiation.
|
|
Was made incorrect by 98a710caf5e907344329ee9e9f7b5fd87c50836f .
|
|
Restores the intended behaviour from v8.3 and earlier.
|
|
|
|
|
|
|
|
|
|
as glued.
Possible improvement: rotate using the left children in the glue function,
so that the iter function becomes mostly tail-recursive. Drawback: two
allocations per glue instead of a single one.
This commit makes the following command go from 7.9s to 3.0s:
coqtop <<< "Require Import BigZ ZBinary Reals OrdersEx. Time SearchPattern _." | tail -n 1
|
|
|
|
|
|
This is actually not so perfect because of the lambdas in the return
clause which we would not like to look in.
|
|
for being able to interpret a "match" as a constr pattern).
|
|
in the presence of let-ins).
|
|
|
|
|
|
|
