| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: gares
|
|
This seems to be a pattern used quite a bit in the wild, it does not hurt
to be a bit more lenient to tolerate this kind of use. Interestingly the
API was already offering a similar generalization in some unrelated places.
We also backtrack on the change in Floats.FloatLemmas since it is an instance
of this phenomenon.
|
|
A pattern-matching clause was missing in 5f314036e4d (PR #11261).
The anomaly triggered in configurations like "fun (x:T) y => ..."
(even in the absence of "Implicit Types").
|
|
|
|
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.
|
|
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>
|
|
We add hexadecimal numerals according to the following regexp
0[xX][0-9a-fA-F][0-9a-fA-F_]*(\.[0-9a-fA-F_]+)?([pP][+-]?[0-9][0-9_]*)?
This is unfortunately a rather large commit. I suggest reading it in
the following order:
* test-suite/output/ZSyntax.{v,out} new test
* test-suite/output/Int63Syntax.{v,out} ''
* test-suite/output/QArithSyntax.{v,out} ''
* test-suite/output/RealSyntax.{v,out} ''
* test-suite/output/FloatSyntax.{v,out} ''
* interp/numTok.ml{i,} extending numeral tokens
* theories/Init/Hexadecimal.v adaptation of Decimal.v
for the new hexadecimal Numeral Notation
* theories/Init/Numeral.v new interface for Numeral Notation (basically,
a numeral is either a decimal or an hexadecimal)
* theories/Init/Nat.v add hexadecimal numeral notation to nat
* theories/PArith/BinPosDef.v '' positive
* theories/ZArith/BinIntDef.v '' Z
* theories/NArith/BinNatDef.v '' N
* theories/QArith/QArith_base.v '' Q
* interp/notation.ml{i,} adapting implementation of numeral notations
* plugins/syntax/numeral.ml ''
* plugins/syntax/r_syntax.ml adapt parser for real numbers
* plugins/syntax/float_syntax.ml adapt parser for primitive floats
* theories/Init/Prelude.v register parser for nat
* adapting the test-suite (test-suite/output/NumeralNotations.{v,out}
and test-suite/output/SearchPattern.out)
* remaining ml files (interp/constrex{tern,pr_ops}.ml where two open
had to be permuted)
|
|
"decimal" would no longer be an appropriate name when extending to
hexadecimal for instance.
|
|
|
|
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.
|
