| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This should make the univbinders output test less fragile as it
depends less on the global counter (still used for universes from
section variables).
|
|
variables in goals
Reviewed-by: SkySkimmer
|
|
of "apply in" fails
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
to 1/2^n
Reviewed-by: VincentSe
|
|
|
|
Fix #12447
|
|
|
|
In a Meta := Evar unification problem and the Meta is bound to a
(named) binder, and the Evar is a GoalEvar, we set the source of the
evar to be the one of the Meta.
|
|
|
|
In this mode, an additional error was emitted, which made the test fail:
Error: There are pending proofs: Unnamed_thm.
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: ejgallego
Ack-by: herbelin
|
|
cf "If this is implemented, long names might cause a printing
problem:" in #11852
|
|
|
|
|
|
The main use case of SearchHead is now handled by headconcl:
The secondary use case was redundant with SearchPattern.
|
|
|
|
|
|
implicit types
Reviewed-by: ejgallego
|
|
Reviewed-by: JasonGross
Ack-by: Zimmi48
Ack-by: herbelin
|
|
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").
|
|
Ack-by: Zimmi48
Reviewed-by: ejgallego
|
|
|
|
|
|
Reviewed-by: ppedrot
|
|
|
|
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)
|
|
multiple scopes for the same inductive)
|
|
Reviewed-by: pi8027
Reviewed-by: zeldovich
|
|
Also `Export ExtrHaskellBasic` in `ExtrHaskellString`.
Fixes #12257
Fixes #12258
|
|
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)
|
|
|
|
Reviewed-by: ejgallego
Reviewed-by: jfehrle
|
|
entries with a global rule
Reviewed-by: ejgallego
Ack-by: gares
|
|
|
|
primitive projections
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
|
|
This makes the API more orthogonal and allows better structure in
future code.
|
|
Reviewed-by: JasonGross
Ack-by: herbelin
|
|
Reviewed-by: Zimmi48
Reviewed-by: jfehrle
Reviewed-by: maximedenes
Ack-by: ppedrot
|
|
This happens in practice with the list syndef in List.v
|
|
We factorize code from declareInd.ml and inductiveops.ml which was
already existing in record.ml.
We keep expansion of local definitions in the type of fields of
primitive records while these are not expanded in the non-primitive
case. This is to be consistent with what Indtypes.compute_projections
is doing. See discussion at #11135.
We keep the unused code from inductiveops.ml for possible future use
though.
Include improvements contributed by Gaëtan Gilbert.
|
|
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.
|
|
While we're at it also compare instances in glob_constr although I
don't know if that changes any behaviour.
|
