| Age | Commit message (Collapse) | Author |
|---|
|
evars
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
|
|
Reviewed-by: herbelin
|
|
|
|
|
|
|
|
Reviewed-by: ppedrot
Ack-by: vbgl
|
|
Reviewed-by: gares
|
|
Reviewed-by: vbgl
|
|
Reviewed-by: Zimmi48
Ack-by: JasonGross
|
|
|
|
|
|
|
|
|
|
|
|
Instead of loading the whole file in memory, we simply load an index table
associating a file position to a key hash. Cache access is then performed
on the fly by unmarshalling the data whose hash corresponds and checking
key equality.
|
|
For some reason it was explicitly deactivated since the file was added, but
I have no idea why. Unsetting sharing would lead to potential explosive
memory consumption at unmarshalling time which is not worth the minimal cost
it has at marshalling time.
|
|
|
|
coercion not being used
Reviewed-by: ejgallego
|
|
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
To tie the knot (since the evar depends on the evar type and the
source of the evar type of the evar), we use an "update_source"
function.
An alternative could be to provide a function to build both an evar
with its evar type directly in evd.ml...
|
|
of universes in "Context"
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
|
The bot merge was changed some time ago.
|
|
|
|
Fixes #13453 which was a loop in
~~~ocaml
let normalize a =
let o = optims () in
let rec norm a =
let a' = if o.opt_kill_dum then kill_dummy (simpl o a) else simpl o a in
if eq_ml_ast a a' then a else norm a'
in norm a
~~~
the `eq_ml_ast` was always returning `false`.
|
|
notations.
Reviewed-by: jfehrle
Reviewed-by: gares
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
|
|
Reviewed-by: ppedrot
|
|
erroneously caught
Reviewed-by: ppedrot
|
|
sense
Reviewed-by: Zimmi48
|
|
|
|
|
|
For constr, this means clarifying that "ident" is deprecated and to be
replaced by "name". Here, some cleaning shall have to be done at the
end of deprecation phase, when "ident" will take its literal meaning.
For custom notations, this is about documenting the effect of "ident"
and "global" which was yet undocumented.
Note that we anticipate an example in constr working with the literal
meaning of "ident" (temporarily silencing the warning).
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
|
|
|
|
|
|
We use a deprecation phase where:
- "ident" means "name" (as it used to mean), except in custom coercion
entries where it already meant "ident".
- "ident" will be made again available (outside situation of
coercions) to mean "ident" at the end of deprecation phase.
Also renaming "as ident" into "as name".
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
|
|
|
|
Fixes #7430 and fixes #10968
This commit makes the following changes:
- Add an exception `Signal` used to convert OCaml signals to exceptions.
`Signal` is registered as critical in `CErrors` to avoid being caught in the
wrong `with` clauses.
- Make `Control.timeout` into a safer interface based on `option` instead of
exceptions.
- Modify `tclTIMEOUT` to fail with `CErrors.Timeout` instead of
`Logic_monad.Tac_timeout`, as was already advertised in the ocamldoc documentation.
- Removes `Logic_monad.Tac_timeout` altogether because it no longer has a use.
|
|
same time (granting #9816)
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
fix #11170).
Reviewed-by: gares
Reviewed-by: xavierleroy
Ack-by: ppedrot
|
|
In #11172, an "=" on the number of arguments of an applied coercion
had become a ">" on the number of arguments of the coercion. It should
have been a ">=". The rest of changes in constrextern.ml is "cosmetic".
Note that in #11172, in the case of a coercion to funclass, the
definition of number of arguments of an applied coercion had moved
from including the extra arguments of the coercion to funclass to
exactly the nomber of arguments of the coercion (excluding the extra
arguments). This was necessary to take into account that several
coercions can be nested, at least of those involving a coercion to
funclass.
Incidentally, we create a dedicated output file for notations and
coercions.
|
|
|
|
The Norm name was confusing enough to have introduced a few kernel
bugs, so it deserved to be changed as suggested in #13274.
Contrarily to what it seemingly meant, it was actually standing
for neutral terms rather than normal ones. I have kept the 4-letter
naming scheme for simplicity and renamed it into Ntrl.
|
|
Reviewed-by: ejgallego
|
|
in notations
Reviewed-by: ejgallego
Ack-by: Zimmi48
Ack-by: jfehrle
|
|
Reviewed-by: erikmd
Reviewed-by: silene
Ack-by: mattam82
Ack-by: Blaisorblade
Ack-by: gares
Ack-by: Zimmi48
Ack-by: SkySkimmer
Ack-by: ejgallego
|
|
|
