| Age | Commit message (Collapse) | Author |
|---|
|
We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.
|
|
It is the only place where it starts making sense in the whole codebase. It also
fits nicely there since there are other functions manipulating this type in that
module.
In any case this type does not belong to the kernel.
|
|
Namely, WrongNumargInductive and WrongNumargConstructor.
|
|
We also simplify the whole process of interpretation of cases pattern
on the way.
|
|
Reviewed-by: Zimmi48
Ack-by: jfehrle
|
|
|
|
|
|
Reviewed-by: ppedrot
|
|
This avoids doing it repeatedly for nothing in intern/extern.
|
|
They are not used there, and removing the redundance of the the case
representation requires access to the environment, so we push their use
further up.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: herbelin
Ack-by: jfehrle
|
|
Reviewed-by: Zimmi48
|
|
|
|
As discussed in the Coq meeting.
|
|
|
|
Most cases should be accounted in proof code, however be wary of paths
where `Global.env ()` is used.
|
|
The syntax is the one of boolean attributes, that is to say
`#[typing($flag={yes,no}]` where `$flag` is one of `guarded`,
`universes`, `positive`.
We had to instrument the pretyper in a few places, it is interesting
that it is doing so many checks.
|
|
This is just an experiment, but makes the uses of the API easier as we
don't mess with the global state anymore.
|
|
We use the new `Declare.Info` structure to uniformly add properties to
the handling of constants. In this case, per-constant typing flags.
The internal code may want to see some further refactoring, including
pushing the flags down to `Safe_typing.add_constant` , but the changes
in the interface should be definitive.
This will allow #12539 and #9004 using attributes.
|
|
Reviewed-by: mattam82
|
|
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.
|
|
|
|
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
|
|
notations.
Reviewed-by: jfehrle
Reviewed-by: gares
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
|
|
erroneously caught
Reviewed-by: ppedrot
|
|
|
|
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.
|
|
We introduce a class of open binders which includes "x", "x:t", "'pat"
and a class of closed binders which includes "x", "(x:t)", "'pat".
|
|
Reviewed-by: gares
|
|
an arity.
Reviewed-by: ppedrot
|
|
After the previous commit, the stm should correctly pass proof
information, thus we make `proof_object` carry it removing a bunch of
internal code.
|
|
Since 8.5, the STM could not delegate proof information it was
contained inside a closure. This could potentially create some
problems, as witnessed in #12586.
Recent refactoring have reified however much of this state, so it
seems a good idea to use bits of the state now, at the cost of
introducing some safeguards in `declare.ml` w.r.t. `Ephemerons`.
|
|
|
|
|
|
We introduce a warning so boolean attributes are expected to be of the
form `attr={yes,no}` or just `attr` (for `yes`).
We update the documentation, test-suite, and changelog.
|
|
Following discussion in https://github.com/coq/coq/pull/12586 , we
extend the syntax `val=string` to support also arbitrary values.
In particular we support boolean ones, or arbitrary key-pair lists.
This complements the current form `val="string"`, and makes more sense
in general.
Current syntax for the boolean version is `attr=yes` or `attr=no`, but
we could be more liberal if desired.
The general new guideline is that `foo(vals)` is reserved for
the case where `vals` is a list, whereas `foo=val` is for attributes
that allow a unique assignment.
This commit only introduces the support, next commits will migrate
some attributes to this new syntax and deprecate the old versions.
|
|
Reviewed-by: mattam82
Reviewed-by: maximedenes
Reviewed-by: jfehrle
Ack-by: gares
Ack-by: Zimmi48
Ack-by: ppedrot
|
|
|
|
Reviewed-by: Zimmi48
|
|
variables.
Reviewed-by: ejgallego
Ack-by: ppedrot
Ack-by: SkySkimmer
|
|
Ack-by: Blaisorblade
Reviewed-by: JasonGross
Reviewed-by: Zimmi48
Ack-by: jfehrle
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: silene
Reviewed-by: gares
Reviewed-by: Zimmi48
|
|
Fix #13300
|
|
|
|
|
|
|
