| Age | Commit message (Collapse) | Author |
|---|
|
|
|
- rename @{u} to @{uu} (u is the default name so using @{u} doesn't
test as much as it should)
- move part of the test using Require to end of the file (when quickly
testing changes this allows to run most of the test without compiling
the Require'd file)
|
|
This allows proper treatment in notations, ie fixes #13303
The "glob" representation of universes (what pretyping sees) contains
only fully interpreted (kernel) universes and unbound universe
ids (for non Strict Universe Declaration).
This means universes need to be understood at intern time, so intern
now has a new "universe binders" argument. We cannot avoid this due to
the following example:
~~~coq
Module Import M. Universe i. End M.
Definition foo@{i} := Type@{i}.
~~~
When interning `Type@{i}` we need to know that `i` is locally bound to
avoid interning it as `M.i`.
Extern has a symmetrical problem:
~~~coq
Module Import M. Universe i. End M.
Polymorphic Definition foo@{i} := Type@{M.i} -> Type@{i}.
Print foo. (* must not print Type@{i} -> Type@{i} *)
~~~
(Polymorphic as otherwise the local `i` will be called `foo.i`)
Therefore extern also takes a universe binders argument.
Note that the current implementation actually replaces local universes
with names at detype type. (Asymmetrical to pretyping which only gets
names in glob terms for dynamically declared univs, although it's
capable of understanding bound univs too)
As such extern only really needs the domain of the universe
binders (ie the set of bound universe ids), we just arbitrarily pass
the whole universe binders to avoid putting `Id.Map.domain` at every
entry point.
Note that if we want to change so that detyping does not name locally
bound univs we would need to pass the reverse universe binders (map
from levels to ids, contained in the ustate ie in the evar map) to
extern.
|
|
|
|
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
|
|
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
|
|
|
|
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
|
|
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
Reviewed-by: ppedrot
|
|
This avoids relying on fragile invariants.
|
|
We at least support a cast at the top of patterns in notations.
|
