| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
Originally, "VernacTime" and "VernacRedirect" were defined like this:
type vernac_expr =
...
| VernacTime of vernac_list
| VernacRedirect of string * vernac_list
...
where
type vernac_list = located_vernac_expr list
Currently, that list always contained one and only one element.
So I propose changing the definition of these two variants in the following way:
| VernacTime of located_vernac_expr
| VernacRedirect of string * located_vernac_expr
which covers all our current needs and enforces the invariant
related to the number of commands that are part of the
"VernacTime" and "VernacRedirect" variants.
|
|
In the original version, ocamldoc markup wasn't used properly thus
ocamldoc output did not in all places make sense.
This commit makes sure that the documentation of the Predicate module
is as clear as the documentation of the Set module (in the standard library).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
On an application (f args) where the head is magic, we first remove Obj.magic
on arguments before continuing with simplifications (that may push magic down
inside the arguments).
For instance, starting with ((Obj.magic f) (Obj.magic (g h))), we now end
with ((Obj.magic f) (g h)) instead of ((Obj.magic f) ((Obj.magic g) h))) as
before.
|
|
Unfortunately, my first attempt at replacing (Obj.magic (fun x -> u) v)
by ((fun x -> Obj.magic u) v) was badly typed, as seen in FingerTree:
the argument v should also be magic now, otherwise it might not have
the same type as x.
This optimization is now correctly done, and to mitigate the potential inflation
of Obj.magic, I've added a few simplification rules to avoid redundant magics,
push them down inside terms, favor the form (Obj.magic f x y z), etc.
|
|
The option is still there, but not documented since it is too
dangerous. Hints and type classes instances are not taking cleared
variables into account.
|
|
|
|
During an extraction, a few tables are maintained to cache
intermediate results. Due to modules, the kernel_name index
for these caching tables aren't enough. For instance, in
bug #3923, a constant is first transparent (from inside the
module) then opaque (when seen from the signature). The previous
protections were actually obsolete (tests via visible_con), we
now checks that the constant_body is still the same.
|
|
Change was introduced by cedcfc9bc386456f3fdd225f739706e4f7a2902c.
|
|
vars by _)
|
|
typing. Had built the instance for substitution in the wrong context.
|
|
cleaning done in e8c47b652a0.
It had no serious consequences except having whd-reduction blocked on
a let-in when typing a return clause with let-ins in the arity (a
priori resulting in return types of the form e.g. "(let x:=t in fun y
=> T) u" instead of T[x:=t;y:=u], if I'm not mistaking).
This fixes 3210.v in test-suite.
|
|
|
|
The unshelve tactical can be used to get the shelved holes. This changes the
proper ordering of holes though, so expect some broken scripts. Also, the
test-suite is not fixed yet.
|
|
|
|
|
|
|
|
|
|
|
|
since the clear_flag is new.
|
|
all cases of rewrite.
|
|
This is done via a unique pass which seems roughly linear in practice,
even on big developments like CompCert. There's a List.nth in an env at
each MLrel, that could be made logarithmic if necessary via Okasaki's
skew list for instance.
Another approach would be to keep names (as a form of documentation), but
prefix them by _ to please OCaml's warnings. For now, let's be radical and
use the _ pattern.
|
|
lablgtk"
This reverts commit 469cb750c6c1aa46f77b2a89a36f79f29aa97073.
|
|
|
|
This fix only handles MLapp(MLmagic(MLlam...),...). Someday, we'll have
to properly investigate the interaction between all the other optimizations
and MLmagic. But well, at least this precise bug is fixed now.
|
|
Force failing when reaching end of file with unterminated comment when
parsing Make (project) file.
|
|
|
|
|
|
In front of "let rec f x y = ... in f n m", if n is now an implicit argument,
then the argument x of the inner fixpoint f is also considered as implicit.
This optimization is rather ad-hoc, since we only handle MLapp(MLfix()) for
now, and the implicit argument should be reused verbatim as argument.
Note that it might happen that x cannot be implicit in f. But in this
case we would have add an error message about n still occurring somewhere...
At least this small heuristic was easy to add, and was sufficient to solve
the part 2 of bug #4243.
|
|
Soon needing a more algebraic view at version numbers...
|
|
|
|
|
|
|
