| Age | Commit message (Collapse) | Author |
|---|
|
Useful for guarding calls to `unfold` or `cbv` to ensure that, e.g.,
`Opaque foo` doesn't break some automation which tries to unfold `foo`.
We have some timeouts in the strategy success file. We should not run
into issues, because we are not really testing how long these take. We
could just as well use `Timeout 60` or longer, we just want to make sure
the file dies more quickly rather than taking over 10^100 steps.
Note that this tactic does not play well with `abstract`; I have a
potentially controversial change that fixes this issue.
One of the lines in the doc comes from
https://github.com/coq/coq/pull/12129#issuecomment-619771556
Co-Authored-By: Pierre-Marie Pédrot <pierre-marie.pedrot@irif.fr>
Co-Authored-By: Théo Zimmermann <theo.zimmermann@inria.fr>
Co-Authored-By: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>
|
|
same inductive)
Numeral Notations now play better with multiple scopes for the same
inductive. Previously, when multiple numeral notations where defined
for the same inductive, only the last one was considered for
printing. Now, we proceed as follows
1. keep only uninterpreters that produce an output (first
List.map_filter)
2. keep only uninterpretation for scopes that either have a scope
delimiter or are open (second List.map_filter)
3. the final selection is made according to the order of open scopes,
(find_uninterpretation) or or according to the last defined
notation if no appropriate scope is open (head of list at the end)
|
|
|
|
in record tuples
Reviewed-by: ejgallego
|
|
entries with a global rule
Reviewed-by: ejgallego
Ack-by: gares
|
|
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.
|
|
Reviewed-by: Zimmi48
Reviewed-by: jfehrle
Reviewed-by: maximedenes
Ack-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
This is due to "global" being a syntactic notation, thus including ident.
Parsing was automatically supporting this. This commit adds support for printing.
|
|
entry.
Parsing was automatically supporting this. This commit adds support for printing.
Note: It would be more delicate to recognize that some given entry
support applicative nodes hence abbreviations with arguments.
|
|
This is to avoid confusion with typing coercions.
No change of semantics.
|
|
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
|
