| Age | Commit message (Collapse) | Author |
|---|
|
This provides linking, appropriate coloring and appropriate hovering
in coqdoc documents.
In particular, this fixes #7697.
|
|
|
|
No change of semantics.
|
|
Reviewed-by: Zimmi48
Reviewed-by: jfehrle
Reviewed-by: maximedenes
Ack-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
While we're at it also compare instances in glob_constr although I
don't know if that changes any behaviour.
|
|
|
|
Co-authored-by: Jasper Hugunin <jasper@hugunin.net>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
Support in the parser needs yet to be added though.
|
|
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.
|
|
Ack-by: herbelin
|
|
Add headers to a few files which were missing them.
|
|
|
|
We make the primitives for backtrace-enriched exceptions canonical in
the `Exninfo` module, deprecating all other aliases.
At some point dependencies between `CErrors` and `Exninfo` were a bit
complex, after recent clean-ups the roles seem much clearer so we can
have a single place for `iraise` and `capture`.
|
|
Reviewed-by: ejgallego
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
This is a case which conventionally deactivates implicit arguments.
|
|
Exception: when the notation is to some @id.
Formerly, this was ignored for all kinds of string notations.
|
|
|
|
|
|
Also apply the same conditions for printing constructors as record
instances in both terms and patterns.
|
|
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.
|
|
This is to match the parsing policy (see #11091).
In particular, we deactivate also argument scopes, consistently with
what is done at parsing time.
|
|
The CApp(CRef f,[]) encoding required to match the NApp(NRef f,[])
encoding of @f was lost.
It remains to let printing match parsing wrt the deactivation of
implicit arguments and argument scopes in such case. See next commit.
|
|
When a non-applied reference was matching a notation to the same
reference, implicit arguments were lost.
|
|
We fix also an index error in deciding when to explicit print a
non-inferable implicit argument.
|
|
Reviewed-by: ejgallego
|
|
Also renamed it to relative_entry_level.
Correspondence between old and new representation is:
(n,L) -> LevelLt n
(n,E), (n,Prec n) -> LevelLe n
(n,Any) -> LevelSome
(n,Prec p) when n<>p was unused
Should not change global semantics (except error message in pr_arg).
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
|
|
explicitly print implicit arguments
Ack-by: SkySkimmer
Reviewed-by: ejgallego
|
|
notation format + new notion of format associated to a given interpretation
Ack-by: maximedenes
|
|
entries)."
This reverts commit 29919b725262dca76708192bde65ce82860747be.
It was pushed by mistake as part of #11530. Sorry about it.
|
|
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.
|
|
This is in anticipation of defining a new type
type specific_notation = LastLonelyNotation | NotationInScope
|
|
|
|
If a return type is given to a match/if/let, then we are in context
(and thus may skip coercions or not make explicit those implicit
arguments inferable from context). Note that the notion of "inferable
from context" remains anyway an approximation in the case of implicit
arguments.
The body of a fix/cofix is also in context.
Also fixed an inconsistency with parsing in the scope used to print
the body of a fix.
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
This was already possible manually using "{ _ }" in the type of
declaration. This was also possible for type classes. So, no reason to
forbid in Arguments.
|
|
|
