| Age | Commit message (Collapse) | Author |
|---|
|
reference.
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
|
|
This allows the following to interpret "0" in the expected scope:
Notation "0" := true : bool_scope.
Axiom f : bool -> bool -> nat.
Record R := { p : bool -> nat }.
Check (@f 0) 0.
Check fun r => r.(@p) 0.
|
|
naming
Ack-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
|
|
|
|
This will allow for instance to check the status of a variable name
used both as a term and binder in notations.
|
|
Currently, global references in patterns used also as terms were
accepted for parsing but not for printing.
We accept section variables for both parsing and printing. We reject
constant and inductive types for both parsing and printing.
Among other, this also fixes a hole in interpreting variables used
both patterns and terms: the term part was not interpreted.
|
|
We accept patterns that we failed to type as a fallback.
|
|
|
|
An alternative could also be to split the initialization of the
environment and the declaration of initial "binders".
|
|
|
|
|
|
|
|
Became unused in e034b4090ca45410853db60ae2a5d2f220b48792
|
|
|
|
Reviewed-by: herbelin
|
|
Persistent arrays expose a functional interface but are implemented
using an imperative data structure. The OCaml implementation is based on
Jean-Christophe Filliâtre's.
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
We interpret `{|proj=pat|}` as `@C _ pat` instead of `C _ pat` (where
the `_` stands for the parameters).
Fix #12534
|
|
|
|
Re-raising inside exception handlers must be done with care in order
to preserve backtraces; even if newer OCaml versions do a better job
in automatically spilling `%reraise` in places that matter, there is
no guarantee for that to happen.
I've done a best-effort pass of places that were re-raising
incorrectly, hopefully I got the logic right.
There is the special case of `Nametab.error_global_not_found` which is
raised many times in response to a `Not_found` error; IMHO this error
should be converted to something more specific, however the scope of
that change would be huge as to do easily...
|
|
Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: gares
|
|
|
|
This is extracted from #9710, where we need the environment anyway to compute
iota rules on inductive types with let-bindings. The commit is self-contained,
so I think it could go directly in to save me a few rebases.
Furthermore, this is also related to #11707. Assuming we split cbn from the
other reduction machine, this allows to merge the "local" machine with
the general one, since after this PR they will have the same type. One less
reduction machine should make people happy.
|
|
constructor.
Moreover, the link to the constructor was hiding other contents of the
tuple.
|
|
This allows to have the "No local fields allowed in a record
construction" error applicable to all fields and not only the first
one. Formerly, this was wrongly raising an error "This record contains
fields of both T and T".
|
|
We basically avoid a detour via intern_applied_reference.
In particular, this stops dumpglobbing the name of the "constructor"
of the record which in practice does not appear in the source.
|
|
This provides linking, appropriate coloring and appropriate hovering
in coqdoc documents.
In particular, this fixes #7697.
|
|
|
|
No change of semantics.
|
|
|
|
|
|
Co-authored-by: Jasper Hugunin <jasper@hugunin.net>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
Four types of numerals are introduced:
- positive natural numbers (may include "_", e.g. to separate thousands, and leading 0)
- integer numbers (may start with a minus sign)
- positive numbers with mantisse and signed exponent
- signed numbers with mantisse and signed exponent
In passing, we clarify that the lexer parses only positive numerals,
but the numeral interpreters may accept signed numerals.
Several improvements and fixes come from Pierre Roux. See
https://github.com/coq/coq/pull/11703 for details. Thanks to him.
|
|
Add headers to a few files which were missing them.
|
|
On the principle that a notation to a constant inherits the implicit
arguments of the constant, a non-applied notation should inherit its
next maximal implicit arguments.
|
|
|
|
|
|
Exception: when the notation is to some @id.
Formerly, this was ignored for all kinds of string notations.
|
|
This is a change of semantics.
|
|
This was done for abbreviations but not string notations. This adopts
the policy proposed in #11091 to make parsing and printing consistent.
|
|
We do two changes:
- We distinguish between a notion of format generically attached to
notations and a new notion of format attached to interpreted
notations. "Reserved Notation" attaches a format
generically. "Notation" attaches the format specifically to the given
interpretation, and additionally, attaches it generically if it is the
first time the notation is defined.
- We warn before overriding an explicitly reserved generic format, or
a specific format.
|
|
The standard use is to repeat the option keywords in lowercase, which
is basically useless.
En passant add doc entry for Dump Arith.
|
|
- Implicit arguments in the return clause and in the branches
of a match were not checked.
- Implicit arguments in each declaration of intern_context were not
restarted.
- Additionally, in intern_context, we take into account ids from the
env on top of which intern_context is called.
- A better approximation of the check for manual implicit in notations
improved (though not fully correct because the exact context of
interpretation of a binder in a notation with recursive binders is
not known).
We also rename impl_binder_index into binder_block_names in anticipation of
checking redundancies also for non-implicit arguments.
|
|
WithoutTypeConstraint says it can be a term. In particular, if it has
manual implicit arguments, these will be allowed only in leading
lambdas. I.e. it can start with "fun {x}" but not with "forall {x}".
New constructor UnknownIfTermOrType allows to be both a term or a
type. In particular, if it allowed start both with "fun {x}" and
"forall {x}".
|
|
+ tests in the test-suite for non max local implicit arguments
|
|
|
|
|
